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 omega : set const SNo : set prop const eps_ : set set axiom SNo_eps_: !x:set.x iIn omega -> SNo (eps_ x) const SNoLt : set set prop term < = SNoLt infix < 2020 2020 const Empty : set axiom SNo_eps_pos: !x:set.x iIn omega -> Empty < eps_ x const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 axiom mul_SNo_pos_pos: !x:set.!y:set.SNo x -> SNo y -> Empty < x -> Empty < y -> Empty < x * y const real : set const ordsucc : set set lemma !x:set.!y:set.x iIn real -> Empty < x -> SNo x -> y iIn omega -> eps_ y * x < ordsucc Empty -> eps_ y iIn real -> Empty < eps_ y * x -> ?z:set.z iIn real & x * z = ordsucc Empty var x:set var y:set hyp x iIn real hyp Empty < x hyp SNo x hyp y iIn omega hyp eps_ y * x < ordsucc Empty claim eps_ y iIn real -> ?z:set.z iIn real & x * z = ordsucc Empty