proposition: Corollary RTop_metrizable: metrizable RTop.
proof: Proof. exists R_metric. - exact R_metric_is_metric. - exact RTop_metrization. Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals