proposition: Lemma open_set_P5 : open_set (fun x:R => True).
proof: Proof. unfold open_set; intros; unfold neighbourhood. exists (mkposreal 1 Rlt_0_1); unfold included; intros; trivial. Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type