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 Repl : set (set set) set const Sing : set set term SetAdjoin = \x:set.\y:set.binunion x (Sing y) const Empty : set const ordsucc : set set term eps_ = \x:set.binunion (Sing Empty) (Repl x \y:set.SetAdjoin (ordsucc y) (Sing (ordsucc Empty))) term SNoElts_ = \x:set.binunion x (Repl x \y:set.SetAdjoin y (Sing (ordsucc Empty))) term nIn = \x:set.\y:set.~ x iIn y term SNo_ = \x:set.\y:set.Subq y (SNoElts_ x) & !z:set.z iIn x -> ~(SetAdjoin z (Sing (ordsucc Empty)) iIn y <-> z iIn y) term SNoElts_ = \x:set.binunion x (Repl x \y:set.SetAdjoin y (Sing (ordsucc Empty))) term SNo_ = \x:set.\y:set.Subq y (SNoElts_ x) & !z:set.z iIn x -> ~(SetAdjoin z (Sing (ordsucc Empty)) iIn y <-> z iIn y) const omega : set const nat_p : set prop axiom omega_nat_p: !x:set.x iIn omega -> nat_p x lemma !x:set.x iIn omega -> nat_p x -> Subq (eps_ x) (SNoElts_ (ordsucc x)) & !y:set.y iIn ordsucc x -> ~(SetAdjoin y (Sing (ordsucc Empty)) iIn eps_ x <-> y iIn eps_ x) claim !x:set.x iIn omega -> SNo_ (ordsucc x) (eps_ x)