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