proposition: Lemma open_set_P1 : forall D:R -> Prop, open_set D <-> D =_D interior D.
proof: Proof. intro; split. - intro; unfold eq_Dom; split. + apply interior_P2; assumption. + apply interior_P1. - intro; unfold eq_Dom in H; elim H; clear H; intros; unfold open_set; intros; unfold included, interior in H; unfold included in H0; apply (H _ H1). Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type