proposition: Lemma adherence_P4 : forall F G:R -> Prop, included F G -> included (adherence F) (adherence G).
proof: Proof. unfold adherence, included; unfold point_adherent; intros; elim (H0 _ H1); unfold intersection_domain; intros; elim H2; clear H2; intros; exists x0; split; [ assumption | apply (H _ H3) ]. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type