const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y axiom In_no2cycle: !x:set.!y:set.x iIn y -> ~ y iIn x axiom In_irref: !x:set.nIn x x const ordsucc : set set axiom ordsuccE: !x:set.!y:set.y iIn ordsucc x -> y iIn x | y = x axiom FalseE: ~ False const ordinal : set prop axiom ordinal_trichotomy_or: !x:set.!y:set.ordinal x -> ordinal y -> x iIn y | x = y | y iIn x var x:set var y:set hyp ordinal x hyp y iIn x claim ordinal (ordsucc y) -> ordsucc y iIn x | x = ordsucc y