const Subq : set set prop const binintersect : set set set axiom binintersect_com_Subq: !x:set.!y:set.Subq (binintersect x y) (binintersect y x) axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y claim !x:set.!y:set.binintersect x y = binintersect y x