const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y const Pi : set (set set) set term setexp = \x:set.\y:set.Pi y \z:set.x term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y const SNo : set prop const add_SNo : set set set term + = add_SNo infix + 2281 2280 axiom SNo_add_SNo: !x:set.!y:set.SNo x -> SNo y -> SNo (x + y) const SNoS_ : set set const omega : set const SNoLt : set set prop term < = SNoLt infix < 2020 2020 const ap : set set set const SNoCut : set set set const Repl : set (set set) set const minus_SNo : set set term - = minus_SNo const SNoLev : set set const SNoEq_ : set set set prop const abs_SNo : set set const eps_ : set set lemma !x:set.!y:set.!z:set.!w:set.SNo x -> y iIn setexp (SNoS_ omega) omega -> z iIn setexp (SNoS_ omega) omega -> (!u:set.u iIn omega -> ap y u < x) -> (!u:set.u iIn omega -> !v:set.v iIn u -> ap y v < ap y u) -> (!u:set.u iIn omega -> x < ap z u) -> (!u:set.u iIn omega -> !v:set.v iIn u -> ap z u < ap z v) -> x = SNoCut (Repl omega (ap y)) (Repl omega (ap z)) -> SNo - x -> (!u:set.u iIn omega -> SNo (ap y u)) -> (!u:set.u iIn omega -> SNo (ap z u)) -> (!u:set.SNo u -> (!v:set.v iIn Repl omega (ap y) -> v < u) -> (!v:set.v iIn Repl omega (ap z) -> u < v) -> Subq (SNoLev (SNoCut (Repl omega (ap y)) (Repl omega (ap z)))) (SNoLev u) & SNoEq_ (SNoLev (SNoCut (Repl omega (ap y)) (Repl omega (ap z)))) (SNoCut (Repl omega (ap y)) (Repl omega (ap z))) u) -> SNoLev x = omega -> w iIn SNoS_ omega -> (!u:set.u iIn omega -> abs_SNo (w + - x) < eps_ u) -> SNoLev w iIn omega -> SNo w -> SNo - w -> SNo (x + - w) -> w = x var x:set var y:set var z:set var w:set hyp SNo x hyp y iIn setexp (SNoS_ omega) omega hyp z iIn setexp (SNoS_ omega) omega hyp !u:set.u iIn omega -> ap y u < x hyp !u:set.u iIn omega -> !v:set.v iIn u -> ap y v < ap y u hyp !u:set.u iIn omega -> x < ap z u hyp !u:set.u iIn omega -> !v:set.v iIn u -> ap z u < ap z v hyp x = SNoCut (Repl omega (ap y)) (Repl omega (ap z)) hyp SNo - x hyp !u:set.u iIn omega -> SNo (ap y u) hyp !u:set.u iIn omega -> SNo (ap z u) hyp !u:set.SNo u -> (!v:set.v iIn Repl omega (ap y) -> v < u) -> (!v:set.v iIn Repl omega (ap z) -> u < v) -> Subq (SNoLev (SNoCut (Repl omega (ap y)) (Repl omega (ap z)))) (SNoLev u) & SNoEq_ (SNoLev (SNoCut (Repl omega (ap y)) (Repl omega (ap z)))) (SNoCut (Repl omega (ap y)) (Repl omega (ap z))) u hyp SNoLev x = omega hyp w iIn SNoS_ omega hyp !u:set.u iIn omega -> abs_SNo (w + - x) < eps_ u hyp SNoLev w iIn omega hyp SNo w claim SNo - w -> w = x