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 Eps_i : (set prop) set term CSNo_Re = \x:set.Eps_i \y:set.SNo y & ?z:set.SNo z & x = SNo_pair y z axiom Eps_i_ex: !p:set prop.(?x:set.p x) -> p (Eps_i p) claim !x:set.CSNo x -> SNo (CSNo_Re x) & ?y:set.SNo y & x = SNo_pair (CSNo_Re x) y