fact: Definition WOSubset_plus_point {X:hSet} (S:WOSubset X) (z:X) (nSz : ¬ S z) : LEM -> WOSubset X := λ lem, subtype_plus S z,, TOSrel (TOSubset_plus_point S z nSz),, TOtotal (TOSubset_plus_point S z nSz),, hasSmallest_WOSubset_plus_point S z nSz lem.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets