proposition: Lemma closed_set_P1 : forall D:R -> Prop, closed_set D <-> D =_D adherence D.
proof: Proof. intro; split. - intro; unfold eq_Dom; split. + apply adherence_P1. + apply adherence_P2; assumption. - unfold eq_Dom; unfold included; intros; assert (H0 := adherence_P3 D); unfold closed_set in H0; unfold closed_set; unfold open_set; unfold open_set in H0; intros; assert (H2 : complementary (adherence D) x). + unfold complementary; unfold complementary in H1; red; intro; elim H; clear H; intros _ H; elim H1; apply (H _ H2). + assert (H3 := H0 _ H2); unfold neighbourhood; unfold neighbourhood in H3; elim H3; intros; exists x0; unfold included; unfold included in H4; intros; assert (H6 := H4 _ H5); unfold complementary in H6; unfold complementary; red; intro; elim H; clear H; intros H _; elim H6; apply (H _ H7). Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type