const In : set set prop term iIn = In infix iIn 2000 2000 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 Empty : set axiom nat_0: nat_p Empty axiom nat_p_omega: !x:set.nat_p x -> x iIn omega const SNo : set prop axiom int_SNo: !x:set.x iIn int -> SNo x const ordsucc : set set axiom mul_SNo_oneL: !x:set.SNo x -> ordsucc Empty * x = x axiom eps_0_1: eps_ Empty = ordsucc Empty claim !x:set.x iIn int -> ?y:set.y iIn omega & ?z:set.z iIn int & x = eps_ y * z