const SNo : set prop const ordsucc : set set const Empty : set axiom SNo_1: SNo (ordsucc Empty) const CSNo_Re : set set axiom SNo_Re: !x:set.SNo x -> CSNo_Re x = x claim CSNo_Re (ordsucc Empty) = ordsucc Empty