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 axiom Subq_ref: !x:set.Subq x x const ordinal : set prop axiom ordinal_TransSet: !x:set.ordinal x -> TransSet x axiom ordinal_trichotomy_or: !x:set.!y:set.ordinal x -> ordinal y -> x iIn y | x = y | y iIn x claim !x:set.!y:set.ordinal x -> ordinal y -> x iIn y | Subq y x