proposition: Corollary RTop_second_countable : second_countable RTop.
proof: Proof. apply (second_countable_subbasis RTop (Union (ImageFamily (fun q => [r : R | r < Q2R q])) (ImageFamily (fun q => [r : R | r > Q2R q])))). 2: { apply countable_union2; now apply countable_img, countable_type_ensemble, Q_countable. } apply RTop_subbasis_rational_beams. Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals