const In : set set prop term iIn = In infix iIn 2000 2000 const SNo : set prop const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 term SNo_max_of = \x:set.\y:set.y iIn x & SNo y & !z:set.z iIn x -> SNo z -> z <= y term nIn = \x:set.\y:set.~ x iIn y term SNo_min_of = \x:set.\y:set.y iIn x & SNo y & !z:set.z iIn x -> SNo z -> y <= z term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y term TransSet = \x:set.!y:set.y iIn x -> Subq y x const nat_p : set prop const ordsucc : set set const Empty : set axiom nat_1: nat_p (ordsucc Empty) const omega : set axiom nat_p_omega: !x:set.nat_p x -> x iIn omega const diadic_rational_p : set prop const eps_ : set set axiom eps_diadic_rational_p: !x:set.x iIn omega -> diadic_rational_p (eps_ x) const add_SNo : set set set term + = add_SNo infix + 2281 2280 axiom add_SNo_diadic_rational_p: !x:set.!y:set.diadic_rational_p x -> diadic_rational_p y -> diadic_rational_p (x + y) const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 axiom mul_SNo_diadic_rational_p: !x:set.!y:set.diadic_rational_p x -> diadic_rational_p y -> diadic_rational_p (x * y) var x:set var y:set var z:set hyp SNo x hyp ~ diadic_rational_p x hyp SNo y hyp SNo z hyp diadic_rational_p y hyp diadic_rational_p z hyp x + x = y + z claim x != eps_ (ordsucc Empty) * (y + z)