Lemma chain_union_le {X:hSet} {I:UU} (S : I -> WOSubset X) (Schain : is_wosubset_chain S) : ∀ i, S i ≼ ⋃ Schain. Proof. intros i. exists (subtype_union_containedIn S i). split. * exact (pr2 (chain_union_tosub_le _ i)). * intros s t Ss Tt. exact (chain_union_rel_initial Schain i (s,,Ss) (t,,Tt)). Defined.
Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.OrderTheory.OrderedSets.OrderedSets.