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 ordinal : set prop axiom ordinal_Hered: !x:set.ordinal x -> !y:set.y iIn x -> ordinal y const ordsucc : set set axiom ordinal_ordsucc: !x:set.ordinal x -> ordinal (ordsucc x) axiom ordsuccI1: !x:set.Subq x (ordsucc x) axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y axiom ordinal_In_Or_Subq: !x:set.!y:set.ordinal x -> ordinal y -> x iIn y | Subq y x lemma !x:set.!y:set.Subq (ordsucc y) x -> Subq x (ordsucc y) -> ordsucc y = x -> ordsucc y iIn ordsucc x var x:set var y:set hyp ordinal x hyp y iIn x claim Subq (ordsucc y) x -> ordsucc y iIn ordsucc x