proposition: Lemma open_set_P6 : forall D1 D2:R -> Prop, open_set D1 -> D1 =_D D2 -> open_set D2.
proof: Proof. unfold open_set; unfold neighbourhood; intros. unfold eq_Dom in H0; elim H0; intros. assert (H4 := H _ (H3 _ H1)). elim H4; intros. exists x0; apply included_trans with D1; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type