const ordinal : set prop const TransSet : set prop axiom ordinal_TransSet: !x:set.ordinal x -> TransSet x const In : set set prop term iIn = In infix iIn 2000 2000 const Subq : set set prop const ordsucc : set set axiom TransSet_ordsucc_In_Subq: !x:set.TransSet x -> !y:set.y iIn x -> Subq (ordsucc y) x claim !x:set.ordinal x -> !y:set.y iIn x -> Subq (ordsucc y) x