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 add_SNo : set set set term + = add_SNo infix + 2281 2280 const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 const eps_ : set set const ordsucc : set set const Empty : set axiom double_eps_1: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> x + x = y + z -> x = eps_ (ordsucc Empty) * (y + z) const diadic_rational_p : set prop lemma !x:set.!y:set.!z:set.SNo x -> ~ diadic_rational_p x -> SNo y -> diadic_rational_p y -> y + z = x + x -> SNo z -> diadic_rational_p z -> x != eps_ (ordsucc Empty) * (y + z) const SNoLev : set set const nat_p : set prop var x:set var y:set var z:set var w:set var u:set hyp nat_p x hyp !v:set.v iIn x -> !x2:set.SNo x2 -> SNoLev x2 = v -> diadic_rational_p x2 hyp SNo y hyp SNoLev y = x hyp ~ diadic_rational_p y hyp SNo z hyp SNoLev w iIn SNoLev y hyp diadic_rational_p z hyp z + u = y + y hyp SNo u hyp SNoLev u iIn SNoLev w claim ~ diadic_rational_p u