proposition: Lemma RTop_separable : separable RTop.
proof: Proof. exists (Im Full_set Q2R); split. 2: exact rationals_dense_in_RTop. apply countable_img. apply countable_type_ensemble. apply Q_countable. Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals