const In : set set prop term iIn = In infix iIn 2000 2000 const omega : set const SNo : set prop axiom omega_SNo: !x:set.x iIn omega -> SNo x const minus_SNo : set set term - = minus_SNo axiom SNo_minus_SNo: !x:set.SNo x -> SNo - x const int : set axiom int_SNo_cases: !p:set prop.(!x:set.x iIn omega -> p x) -> (!x:set.x iIn omega -> p - x) -> !x:set.x iIn int -> p x claim !x:set.x iIn int -> SNo x