const SNo_pair : set set set const Empty : set const ordsucc : set set term Complex_i = SNo_pair Empty (ordsucc Empty) const SNo : set prop axiom SNo_0: SNo Empty axiom SNo_1: SNo (ordsucc Empty) const CSNo_Im : set set axiom CSNo_Im2: !x:set.!y:set.SNo x -> SNo y -> CSNo_Im (SNo_pair x y) = y claim CSNo_Im Complex_i = ordsucc Empty