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 const nat_p : set prop const ordinal : set prop axiom nat_p_ordinal: !x:set.nat_p x -> ordinal x const SNo : set prop const Empty : set axiom SNo_0: SNo Empty const ordsucc : set set axiom nat_0_in_ordsucc: !x:set.nat_p x -> Empty iIn ordsucc x const SNoLev : set set axiom SNoLev_0: SNoLev Empty = Empty const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 axiom ordinal_SNoLev_max_2: !x:set.ordinal x -> !y:set.SNo y -> SNoLev y iIn ordsucc x -> y <= x const real : set const omega : set const eps_ : set set const exp_SNo_nat : set set set const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 lemma !x:set.!y:set.!z:set.y iIn real -> SNo x -> z iIn omega -> eps_ z <= x -> nat_p (exp_SNo_nat (ordsucc (ordsucc Empty)) z) -> SNo (exp_SNo_nat (ordsucc (ordsucc Empty)) z) -> Empty <= exp_SNo_nat (ordsucc (ordsucc Empty)) z -> ?w:set.w iIn omega & y <= w * x var x:set var y:set var z:set hyp y iIn real hyp SNo x hyp z iIn omega hyp eps_ z <= x hyp nat_p (exp_SNo_nat (ordsucc (ordsucc Empty)) z) claim SNo (exp_SNo_nat (ordsucc (ordsucc Empty)) z) -> ?w:set.w iIn omega & y <= w * x