Lemma chain_union_tosub_le {X : hSet} {I : UU} {S : I → WOSubset X} (Schain : is_wosubset_chain S) (i:I) (inc := subtype_inc (subtype_union_containedIn S i)) : ( S i ≼ ⋃ Schain ) % tosubset. Proof. exists (subtype_union_containedIn S i). intros s s' j. set (u := subtype_inc (λ x J, hinhpr (i,, J)) s : ⋃ Schain). set (u':= subtype_inc (λ x J, hinhpr (i,, J)) s': ⋃ Schain). change (chain_union_rel Schain u u'). assert (q := chain_union_rel_eqn Schain u u' i (pr2 s) (pr2 s')). rewrite q; clear q. exact j. 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.