const nat_p : set prop const ordsucc : set set const Empty : set axiom nat_1: nat_p (ordsucc Empty) const In : set set prop term iIn = In infix iIn 2000 2000 const omega : set axiom nat_p_omega: !x:set.nat_p x -> x iIn omega const SNo : set prop const eps_ : set set axiom SNo_eps_: !x:set.x iIn omega -> SNo (eps_ x) claim SNo (eps_ (ordsucc Empty))