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 Subq : set set prop const binunion : set set set axiom Subq_binunion_eq: !x:set.!y:set.Subq x y = (binunion x y = y) axiom binunion_com: !x:set.!y:set.binunion x y = binunion y x axiom ordinal_linear: !x:set.!y:set.ordinal x -> ordinal y -> Subq x y | Subq y x claim !x:set.!y:set.ordinal x -> ordinal y -> ordinal (binunion x y)