const nat_p : set prop const ordinal : set prop axiom nat_p_ordinal: !x:set.nat_p x -> ordinal x const ordsucc : set set axiom ordinal_ordsucc: !x:set.ordinal x -> ordinal (ordsucc x) const In : set set prop term iIn = In infix iIn 2000 2000 const omega : set const SNo_ : set set prop const eps_ : set set axiom SNo__eps_: !x:set.x iIn omega -> SNo_ (ordsucc x) (eps_ x) const SNo : set prop axiom SNo_SNo: !x:set.ordinal x -> !y:set.SNo_ x y -> SNo y var x:set hyp x iIn omega claim nat_p x -> SNo (eps_ x)