const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y const omega : set const SNo : set prop axiom omega_SNo: !x:set.x iIn omega -> SNo x const nat_p : set prop axiom omega_nat_p: !x:set.x iIn omega -> nat_p x const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom SNoLt_tra: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> x < y -> y < z -> x < z const minus_SNo : set set term - = minus_SNo axiom SNo_minus_SNo: !x:set.SNo x -> SNo - x axiom minus_SNo_Lt_contra: !x:set.!y:set.SNo x -> SNo y -> x < y -> - y < - x axiom SNoLt_trichotomy_or_impred: !x:set.!y:set.SNo x -> SNo y -> !P:prop.(x < y -> P) -> (x = y -> P) -> (y < x -> P) -> P const SNoS_ : set set const ordsucc : set set axiom SNoS_ordsucc_omega_bdd_below: !x:set.x iIn SNoS_ (ordsucc omega) -> - omega < x -> ?y:set.y iIn omega & - y < x axiom SNoS_ordsucc_omega_bdd_above: !x:set.x iIn SNoS_ (ordsucc omega) -> x < omega -> ?y:set.y iIn omega & x < y const add_SNo : set set set term + = add_SNo infix + 2281 2280 const Empty : set var x:set hyp x iIn SNoS_ (ordsucc omega) hyp - omega < x hyp x < omega hyp SNo x hyp nIn x (SNoS_ omega) claim (!y:set.nat_p y -> - y < x -> x < y -> ?z:set.z iIn SNoS_ omega & (z < x & x < z + ordsucc Empty)) -> ?y:set.y iIn SNoS_ omega & (y < x & x < y + ordsucc Empty)