const CSNo : set prop const SNo : set prop const CSNo_Im : set set const SNo_pair : set set set const CSNo_Re : set set axiom CSNo_Im1: !x:set.CSNo x -> SNo (CSNo_Im x) & x = SNo_pair (CSNo_Re x) (CSNo_Im x) claim !x:set.CSNo x -> SNo (CSNo_Im x)