proposition: Lemma interior_P2 : forall D:R -> Prop, open_set D -> included D (interior D).
proof: Proof. intros; unfold open_set in H; unfold included; intros; assert (H1 := H _ H0); unfold interior; apply H1. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type