proposition: Lemma exists_smallest_ordinal_without : forall (p:EP), (exists x : E, (is_ordinal x & ~ p x))-> exists o:E, (is_ordinal o & ~ p o & forall y : E, inc y o -> p y).
proof: Proof. ir. util (exists_smallest_ordinal_with (p:= fun x => (is_ordinal x &~p x))). nin H; ee. sh x; ee; am. nin H0. uh H0. ee. sh x. ee; try am. ir. ap excluded_middle; uhg; ir. assert (x = y). ap extensionality. ap H2. apply ordinal_inc_ordinal with x. am. am. ee. apply ordinal_inc_ordinal with x; am. am. ap ordinal_inc_sub. am. am. apply ordinal_not_inc_itself with x. am. wri H6 H4; am. Qed.
imports: Arith transfinite