proposition: Proposition approximating_family_way_below (x : X) (i : approximating_family x) : approximating_family x i ≪ x.
proof: Proof. exact (pr12 (CX x) i). Qed.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.WayBelow