proposition: Lemma adherence_P1 : forall D:R -> Prop, included D (adherence D).
proof: Proof. intro; unfold included; intros; unfold adherence; unfold point_adherent; intros; exists x; unfold intersection_domain; split. - unfold neighbourhood in H0; elim H0; intros; unfold included in H1; apply H1; unfold disc; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply (cond_pos x0). - apply H. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type