const SNo : set prop const SNo_pair : set set set term CSNo = \x:set.?y:set.SNo y & ?z:set.SNo z & x = SNo_pair y z const Empty : set axiom SNo_0: SNo Empty axiom SNo_pair_0: !x:set.SNo_pair x Empty = x claim !x:set.SNo x -> ?y:set.SNo y & ?z:set.SNo z & x = SNo_pair y z