const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x 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) lemma !x:set.!y:set.ordinal x -> y iIn x -> ordinal (ordsucc y) -> ordsucc y iIn x | x = ordsucc y claim !x:set.!y:set.ordinal x -> y iIn x -> ordsucc y iIn x | x = ordsucc y