proposition: Lemma interior_P1 : forall D:R -> Prop, included (interior D) D.
proof: Proof. intros; unfold included; unfold interior; intros; unfold neighbourhood in H; elim H; intros; unfold included in H0; apply H0; unfold disc; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply (cond_pos x0). Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type