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 int : set const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 const eps_ : set set term diadic_rational_p = \x:set.?y:set.y iIn omega & ?z:set.z iIn int & x = eps_ y * z const nat_p : set prop const ordsucc : set set const Empty : set axiom nat_1: nat_p (ordsucc Empty) axiom nat_p_omega: !x:set.nat_p x -> x iIn omega axiom Subq_omega_int: Subq omega int const SNo : set prop axiom SNo_eps_: !x:set.x iIn omega -> SNo (eps_ x) axiom mul_SNo_oneR: !x:set.SNo x -> x * ordsucc Empty = x claim !x:set.x iIn omega -> ?y:set.y iIn omega & ?z:set.z iIn int & eps_ x = eps_ y * z