const TransSet : set prop const In : set set prop term iIn = In infix iIn 2000 2000 term ordinal = \x:set.TransSet x & !y:set.y iIn x -> TransSet y const ordsucc : set set axiom TransSet_ordsucc: !x:set.TransSet x -> TransSet (ordsucc x) axiom ordsuccE: !x:set.!y:set.y iIn ordsucc x -> y iIn x | y = x claim !x:set.ordinal x -> TransSet (ordsucc x) & !y:set.y iIn ordsucc x -> TransSet y