proposition: Lemma TOSubset_plus_point_initial {X:hSet} (S:TOSubset X) (z:X) (nSz : ¬ S z) : sub_initial (TOSubset_plus_point_incl S z nSz).
proof: Proof. intros s t Ss Tt le. apply (squash_to_hProp Tt); intros [St|ezt]. - exact St. - induction ezt, (ishinh_irrel (ii2 (idpath z)) Tt); change empty in le. exact (fromempty le). Defined.
imports: UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.AxiomOfChoice UniMath.Combinatorics.OrderedSets