const CSNo : set prop const SNo : set prop const CSNo_Re : set set const SNo_pair : set set set axiom CSNo_Re1: !x:set.CSNo x -> SNo (CSNo_Re x) & ?y:set.SNo y & x = SNo_pair (CSNo_Re x) y claim !x:set.CSNo x -> SNo (CSNo_Re x)