Proposition compact_approximating_family_way_below (x : X) (i : compact_approximating_family x) : compact_approximating_family x i ≪ x. Proof. refine (trans_way_below_le (is_compact_approximating_family x i) _). exact (pr122 (AX 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. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.