const In : set set prop term iIn = In infix iIn 2000 2000 const Subq : set set prop term TransSet = \x:set.!y:set.y iIn x -> Subq y x const ordinal : set prop axiom ordinal_TransSet: !x:set.ordinal x -> TransSet x axiom ordinal_In_Or_Subq: !x:set.!y:set.ordinal x -> ordinal y -> x iIn y | Subq y x claim !x:set.!y:set.ordinal x -> ordinal y -> Subq x y | Subq y x