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. 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.
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.