const In : set set prop term iIn = In infix iIn 2000 2000 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 Pi : set (set set) set term setexp = \x:set.\y:set.Pi y \z:set.x const SNo : set prop const SNoLt : set set prop term < = SNoLt infix < 2020 2020 term SNoCutP = \x:set.\y:set.(!z:set.z iIn x -> SNo z) & (!z:set.z iIn y -> SNo z) & !z:set.z iIn x -> !w:set.w iIn y -> z < w term nIn = \x:set.\y:set.~ x iIn y axiom SNoLt_irref: !x:set.~ x < x const SNoS_ : set set const omega : set const abs_SNo : set set const add_SNo : set set set term + = add_SNo infix + 2281 2280 const minus_SNo : set set term - = minus_SNo const ap : set set set const eps_ : set set const SNoCut : set set set const Sep : set (set prop) set const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 var x:set var y:set var z:set var w:set hyp !u:set.u iIn omega -> SNo (ap y u) hyp SNo (SNoCut (Sep (SNoS_ omega) \u:set.?v:set.v iIn omega & u < ap x v) (Sep (SNoS_ omega) \u:set.?v:set.v iIn omega & ap y v < u)) hyp !u:set.u iIn omega -> SNoCut (Sep (SNoS_ omega) \v:set.?x2:set.x2 iIn omega & v < ap x x2) (Sep (SNoS_ omega) \v:set.?x2:set.x2 iIn omega & ap y x2 < v) <= ap y u hyp z iIn SNoS_ omega hyp !u:set.u iIn omega -> abs_SNo (z + - SNoCut (Sep (SNoS_ omega) \v:set.?x2:set.x2 iIn omega & v < ap x x2) (Sep (SNoS_ omega) \v:set.?x2:set.x2 iIn omega & ap y x2 < v)) < eps_ u hyp SNo z hyp w iIn omega hyp ap y w < z hyp !u:set.u iIn SNoS_ omega -> (!v:set.v iIn omega -> abs_SNo (u + - ap y w) < eps_ v) -> u = ap y w claim z != ap y w