const ordinal : set prop const omega : set axiom omega_ordinal: ordinal omega const In : set set prop term iIn = In infix iIn 2000 2000 const nat_p : set prop axiom omega_nat_p: !x:set.x iIn omega -> nat_p x const SNo : set prop const SNoLev : set set const diadic_rational_p : set prop axiom SNoS_omega_diadic_rational_p_lem: !x:set.nat_p x -> !y:set.SNo y -> SNoLev y = x -> diadic_rational_p y const SNoS_ : set set const SNo_ : set set prop axiom SNoS_E2: !x:set.ordinal x -> !y:set.y iIn SNoS_ x -> !P:prop.(SNoLev y iIn x -> ordinal (SNoLev y) -> SNo y -> SNo_ (SNoLev y) y -> P) -> P claim !x:set.x iIn SNoS_ omega -> diadic_rational_p x