const Subq : set set prop const Empty : set axiom Subq_Empty: !x:set.Subq Empty x axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y claim !x:set.Subq x Empty -> x = Empty