const In : set set prop term iIn = In infix iIn 2000 2000 const real : set const SNo : set prop axiom real_SNo: !x:set.x iIn real -> SNo x const Empty : set const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 const ordsucc : set set lemma !x:set.x iIn real -> x != Empty -> SNo x -> ?y:set.y iIn real & x * y = ordsucc Empty claim !x:set.x iIn real -> x != Empty -> ?y:set.y iIn real & x * y = ordsucc Empty