const ordinal : set prop const SNo_ : set set prop term SNo = \x:set.?y:set.ordinal y & SNo_ y x const Eps_i : (set prop) set term SNoLev = \x:set.Eps_i \y:set.ordinal y & SNo_ y x axiom Eps_i_ex: !p:set prop.(?x:set.p x) -> p (Eps_i p) claim !x:set.SNo x -> ordinal (SNoLev x) & SNo_ (SNoLev x) x