Lemma chain_union_WOSubset {X:hSet} {I:UU} {S : I -> WOSubset X} (Schain : is_wosubset_chain S) : WOSubset X. Proof. exists (⋃ Schain). exists (chain_union_rel Schain). repeat split. - apply chain_union_rel_istrans. - apply chain_union_rel_isrefl. - apply chain_union_rel_isantisymm. - apply chain_union_rel_istotal. - apply chain_union_rel_hasSmallest. 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.