const Sep : set (set prop) set const SNoS_ : set set const SNoLev : set set const SNoLt : set set prop term < = SNoLt infix < 2020 2020 term SNoR = \x:set.Sep (SNoS_ (SNoLev x)) (SNoLt x) const SNo : set prop const ordinal : set prop axiom SNoLev_ordinal: !x:set.SNo x -> ordinal (SNoLev x) const In : set set prop term iIn = In infix iIn 2000 2000 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 SepE: !x:set.!p:set prop.!y:set.y iIn Sep x p -> y iIn x & p y claim !x:set.SNo x -> !y:set.y iIn SNoR x -> !P:prop.(SNo y -> SNoLev y iIn SNoLev x -> x < y -> P) -> P