const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y const ordinal : set prop const SNo : set prop axiom ordinal_SNo: !x:set.ordinal x -> SNo x const omega : set const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 const minus_SNo : set set term - = minus_SNo const int : set lemma !x:set.!y:set.x iIn omega -> SNo x -> y iIn omega -> ordinal y -> SNo y -> (- x) * y iIn int const nat_p : set prop var x:set var y:set hyp x iIn omega hyp SNo x hyp y iIn omega hyp nat_p y claim ordinal y -> (- x) * y iIn int