const SNo : set prop const Empty : set axiom SNo_0: SNo Empty const CSNo : set prop axiom SNo_CSNo: !x:set.SNo x -> CSNo x claim CSNo Empty