proposition: Lemma R_upper_beam_open : forall p, @open RTop [r : R | r > p].
proof: Proof. intro. replace [r : R | r > p] with [y : R | p <= y /\ y <> p] by (extensionality_ensembles; constructor; lra). rewrite <- family_union_singleton. repeat (constructor + destruct H). Qed.
imports: TopologicalSpaces OrderTopology MetricSpaces Coq(Lra Lia) ZornsLemma(EnsemblesTactics FiniteIntersections) RationalsInReals