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 : set prop axiom CSNo_I: !x:set.!y:set.SNo x -> SNo y -> CSNo (SNo_pair x y) claim CSNo Complex_i