proposition: Lemma chain_union_le {X:hSet} {I:UU} (S : I -> WOSubset X) (Schain : is_wosubset_chain S) : ∀ i, S i ≼ ⋃ Schain.
proof: 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.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets