proposition: Proposition continuous_dcpo_struct_approx_le_to_le {x y : X} (p : ∏ (i : approximating_family CX x), approximating_family CX x i ⊑ y) : x ⊑ y.
proof: Proof. rewrite <- (approximating_family_lub CX x). use dcpo_lub_is_least. exact p. Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.WayBelow