const SNo : set prop const Empty : set axiom SNo_0: SNo Empty const CSNo_Im : set set axiom SNo_Im: !x:set.SNo x -> CSNo_Im x = Empty claim CSNo_Im Empty = Empty