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 term ordinal = \x:set.TransSet x & !y:set.y iIn x -> TransSet y const binintersect : set set set axiom binintersect_Subq_eq_1: !x:set.!y:set.Subq x y -> binintersect x y = x axiom binintersect_com: !x:set.!y:set.binintersect x y = binintersect y 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 -> ordinal (binintersect x y)