const Pi : set (set set) set term setexp = \x:set.\y:set.Pi y \z:set.x const SNo : set prop const SNoCutP : set set prop const SNoL : set set const SNoR : set set axiom SNoCutP_SNoL_SNoR: !x:set.SNo x -> SNoCutP (SNoL x) (SNoR x) const In : set set prop term iIn = In infix iIn 2000 2000 const real : set const SNoLev : set set const SNoS_ : set set const omega : set axiom SNoLev_In_real_SNoS_omega: !x:set.x iIn real -> !y:set.SNo y -> SNoLev y iIn SNoLev x -> y iIn SNoS_ omega const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom SNoL_E: !x:set.SNo x -> !y:set.y iIn SNoL x -> !P:prop.(SNo y -> SNoLev y iIn SNoLev x -> y < x -> P) -> P axiom SNoR_E: !x:set.SNo x -> !y:set.y iIn SNoR x -> !P:prop.(SNo y -> SNoLev y iIn SNoLev x -> x < y -> P) -> P const Repl : set (set set) set axiom ReplE_impred: !x:set.!f:set set.!y:set.y iIn Repl x f -> !P:prop.(!z:set.z iIn x -> y = f z -> P) -> P const SNoCut : set set set axiom SNo_eta: !x:set.SNo x -> x = SNoCut (SNoL x) (SNoR x) axiom SNoCut_ext: !x:set.!y:set.!z:set.!w:set.SNoCutP x y -> SNoCutP z w -> (!u:set.u iIn x -> u < SNoCut z w) -> (!u:set.u iIn y -> SNoCut z w < u) -> (!u:set.u iIn z -> u < SNoCut x y) -> (!u:set.u iIn w -> SNoCut x y < u) -> SNoCut x y = SNoCut z w const ap : set set set const ordsucc : set set axiom SNo_approx_real_lem: !x:set.x iIn setexp (SNoS_ omega) omega -> !y:set.y iIn setexp (SNoS_ omega) omega -> (!z:set.z iIn omega -> !w:set.w iIn omega -> ap x z < ap y w) -> !P:prop.(SNoCutP (Repl omega (ap x)) (Repl omega (ap y)) -> SNo (SNoCut (Repl omega (ap x)) (Repl omega (ap y))) -> SNoLev (SNoCut (Repl omega (ap x)) (Repl omega (ap y))) iIn ordsucc omega -> SNoCut (Repl omega (ap x)) (Repl omega (ap y)) iIn SNoS_ (ordsucc omega) -> (!z:set.z iIn omega -> ap x z < SNoCut (Repl omega (ap x)) (Repl omega (ap y))) -> (!z:set.z iIn omega -> SNoCut (Repl omega (ap x)) (Repl omega (ap y)) < ap y z) -> P) -> P const add_SNo : set set set term + = add_SNo infix + 2281 2280 const eps_ : set set const minus_SNo : set set term - = minus_SNo const abs_SNo : set set lemma !x:set.!P:prop.!y:set.!z:set.x iIn real -> (!w:set.w iIn setexp (SNoS_ omega) omega -> !u:set.u iIn setexp (SNoS_ omega) omega -> (!v:set.v iIn omega -> ap w v < x) -> (!v:set.v iIn omega -> x < ap w v + eps_ v) -> (!v:set.v iIn omega -> !x2:set.x2 iIn v -> ap w x2 < ap w v) -> (!v:set.v iIn omega -> (ap u v + - eps_ v) < x) -> (!v:set.v iIn omega -> x < ap u v) -> (!v:set.v iIn omega -> !x2:set.x2 iIn v -> ap u v < ap u x2) -> SNoCutP (Repl omega (ap w)) (Repl omega (ap u)) -> x = SNoCut (Repl omega (ap w)) (Repl omega (ap u)) -> P) -> SNo x -> (!w:set.w iIn SNoS_ omega -> (!u:set.u iIn omega -> abs_SNo (w + - x) < eps_ u) -> w = x) -> y iIn setexp (SNoS_ omega) omega -> (!w:set.w iIn omega -> ap y w < x & x < ap y w + eps_ w & !u:set.u iIn w -> ap y u < ap y w) -> z iIn setexp (SNoS_ omega) omega -> (!w:set.w iIn omega -> SNo (ap y w)) -> (!w:set.w iIn omega -> SNo (ap z w)) -> (!w:set.w iIn omega -> ap y w < x) -> (!w:set.w iIn omega -> x < ap y w + eps_ w) -> (!w:set.w iIn omega -> !u:set.u iIn w -> ap y u < ap y w) -> (!w:set.w iIn omega -> (ap z w + - eps_ w) < x) -> (!w:set.w iIn omega -> x < ap z w) -> (!w:set.w iIn omega -> !u:set.u iIn w -> ap z w < ap z u) -> SNoCutP (Repl omega (ap y)) (Repl omega (ap z)) -> SNo (SNoCut (Repl omega (ap y)) (Repl omega (ap z))) -> (!w:set.w iIn omega -> ap y w < SNoCut (Repl omega (ap y)) (Repl omega (ap z))) -> (!w:set.w iIn omega -> SNoCut (Repl omega (ap y)) (Repl omega (ap z)) < ap z w) -> x = SNoCut (Repl omega (ap y)) (Repl omega (ap z)) -> P lemma !x:set.!y:set.!z:set.!w:set.x iIn real -> SNo x -> (!u:set.u iIn SNoS_ omega -> (!v:set.v iIn omega -> abs_SNo (u + - x) < eps_ v) -> u = x) -> (!u:set.u iIn omega -> ap y u < x & x < ap y u + eps_ u & !v:set.v iIn u -> ap y v < ap y u) -> (!u:set.u iIn omega -> SNo (ap y u)) -> SNo (SNoCut (Repl omega (ap y)) (Repl omega (ap z))) -> (!u:set.u iIn omega -> ap y u < SNoCut (Repl omega (ap y)) (Repl omega (ap z))) -> SNo w -> SNoLev w iIn SNoLev x -> w < x -> w iIn SNoS_ omega -> w < SNoCut (Repl omega (ap y)) (Repl omega (ap z)) lemma !x:set.!y:set.!z:set.!w:set.x iIn real -> SNo x -> (!u:set.u iIn SNoS_ omega -> (!v:set.v iIn omega -> abs_SNo (u + - x) < eps_ v) -> u = x) -> (!u:set.u iIn omega -> SNo (ap z u)) -> (!u:set.u iIn omega -> (ap z u + - eps_ u) < x) -> SNo (SNoCut (Repl omega (ap y)) (Repl omega (ap z))) -> (!u:set.u iIn omega -> SNoCut (Repl omega (ap y)) (Repl omega (ap z)) < ap z u) -> SNo w -> SNoLev w iIn SNoLev x -> x < w -> w iIn SNoS_ omega -> SNoCut (Repl omega (ap y)) (Repl omega (ap z)) < w var x:set var P:prop var y:set var z:set hyp x iIn real hyp !w:set.w iIn setexp (SNoS_ omega) omega -> !u:set.u iIn setexp (SNoS_ omega) omega -> (!v:set.v iIn omega -> ap w v < x) -> (!v:set.v iIn omega -> x < ap w v + eps_ v) -> (!v:set.v iIn omega -> !x2:set.x2 iIn v -> ap w x2 < ap w v) -> (!v:set.v iIn omega -> (ap u v + - eps_ v) < x) -> (!v:set.v iIn omega -> x < ap u v) -> (!v:set.v iIn omega -> !x2:set.x2 iIn v -> ap u v < ap u x2) -> SNoCutP (Repl omega (ap w)) (Repl omega (ap u)) -> x = SNoCut (Repl omega (ap w)) (Repl omega (ap u)) -> P hyp SNo x hyp !w:set.w iIn SNoS_ omega -> (!u:set.u iIn omega -> abs_SNo (w + - x) < eps_ u) -> w = x hyp y iIn setexp (SNoS_ omega) omega hyp !w:set.w iIn omega -> ap y w < x & x < ap y w + eps_ w & !u:set.u iIn w -> ap y u < ap y w hyp z iIn setexp (SNoS_ omega) omega hyp !w:set.w iIn omega -> SNo (ap y w) hyp !w:set.w iIn omega -> SNo (ap z w) hyp !w:set.w iIn omega -> ap y w < x hyp !w:set.w iIn omega -> x < ap y w + eps_ w hyp !w:set.w iIn omega -> !u:set.u iIn w -> ap y u < ap y w hyp !w:set.w iIn omega -> (ap z w + - eps_ w) < x hyp !w:set.w iIn omega -> x < ap z w hyp !w:set.w iIn omega -> !u:set.u iIn w -> ap z w < ap z u claim (!w:set.w iIn omega -> !u:set.u iIn omega -> ap y w < ap z u) -> P