const Subq : set set prop const binintersect : set set set axiom binintersect_Subq_2: !x:set.!y:set.Subq (binintersect x y) y axiom binintersect_Subq_1: !x:set.!y:set.Subq (binintersect x y) x axiom binintersect_Subq_max: !x:set.!y:set.!z:set.Subq z x -> Subq z y -> Subq z (binintersect x y) claim !x:set.!y:set.Subq (binintersect x y) (binintersect y x)