proposition: Lemma adherence_P2 : forall D:R -> Prop, closed_set D -> included (adherence D) D.
proof: Proof. unfold closed_set; unfold open_set, complementary; intros; unfold included, adherence; intros; assert (H1 := classic (D x)); elim H1; intro. - assumption. - assert (H3 := H _ H2); assert (H4 := H0 _ H3); elim H4; intros; unfold intersection_domain in H5; elim H5; intros; elim H6; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type