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