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 SNo : set prop const SNoLev : set set const SNoS_ : set set axiom SNoS_I2: !x:set.!y:set.SNo x -> SNo y -> SNoLev x iIn SNoLev y -> x iIn SNoS_ (SNoLev y) const SNoL : set set const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom SNoL_E: !x:set.SNo x -> !y:set.y iIn SNoL x -> !P:prop.(SNo y -> SNoLev y iIn SNoLev x -> y < x -> P) -> P const ordinal : set prop axiom ordinal_SNoLev_max: !x:set.ordinal x -> !y:set.SNo y -> SNoLev y iIn x -> y < x axiom SNoL_I: !x:set.SNo x -> !y:set.SNo y -> SNoLev y iIn SNoLev x -> y < x -> y iIn SNoL x 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 axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y var x:set hyp ordinal x hyp SNo x claim SNoLev x = x -> SNoL x = SNoS_ x