const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y const binunion : set set set const Sing : set set const Empty : set const Repl : set (set set) set const SetAdjoin : set set set const ordsucc : set set term eps_ = \x:set.binunion (Sing Empty) (Repl x \y:set.SetAdjoin (ordsucc y) (Sing (ordsucc Empty))) const SNo : set prop const SNoLev : set set axiom SNoLev_0_eq_0: !x:set.SNo x -> SNoLev x = Empty -> x = Empty axiom FalseE: ~ False axiom ordsuccI2: !x:set.x iIn ordsucc x const nat_p : set prop axiom nat_ordsucc_trans: !x:set.nat_p x -> !y:set.y iIn ordsucc x -> Subq y x const omega : set axiom nat_p_omega: !x:set.nat_p x -> x iIn omega axiom SNo_eps_: !x:set.x iIn omega -> SNo (eps_ x) axiom SNoLev_eps_: !x:set.x iIn omega -> SNoLev (eps_ x) = ordsucc x const SNoEq_ : set set set prop axiom SNoEq_sym_: !x:set.!y:set.!z:set.SNoEq_ x y z -> SNoEq_ x z y axiom nat_ordsucc: !x:set.nat_p x -> nat_p (ordsucc x) axiom nat_p_trans: !x:set.nat_p x -> !y:set.y iIn x -> nat_p y const ordinal : set prop axiom nat_p_ordinal: !x:set.nat_p x -> ordinal x axiom SNoEq_I: !x:set.!y:set.!z:set.(!w:set.w iIn x -> (w iIn y <-> w iIn z)) -> SNoEq_ x y z axiom SNoEq_tra_: !x:set.!y:set.!z:set.!w:set.SNoEq_ x y z -> SNoEq_ x z w -> SNoEq_ x y w axiom SNo_eq: !x:set.!y:set.SNo x -> SNo y -> SNoLev x = SNoLev y -> SNoEq_ (SNoLev x) x y -> x = y axiom nat_inv: !x:set.nat_p x -> x = Empty | ?y:set.nat_p y & x = ordsucc y const SNoLt : set set prop term < = SNoLt infix < 2020 2020 lemma !x:set.Empty < x -> SNo x -> SNoLev x = Empty -> x != Empty lemma !x:set.!y:set.!z:set.nat_p y -> z iIn ordsucc y -> ordinal z -> (z iIn eps_ x <-> z iIn eps_ y) var x:set var y:set hyp nat_p x hyp Empty < y hyp SNoEq_ (SNoLev y) (eps_ x) y hyp SNoLev y iIn ordsucc x hyp SNo y claim nat_p (SNoLev y) -> ?z:set.z iIn x & y = eps_ z