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 SNoL = \x:set.Sep (SNoS_ (SNoLev x)) \y:set.y < x const SNo : set prop const In : set set prop term iIn = In infix iIn 2000 2000 axiom SNoS_I2: !x:set.!y:set.SNo x -> SNo y -> SNoLev x iIn SNoLev y -> x iIn SNoS_ (SNoLev y) axiom SepI: !x:set.!p:set prop.!y:set.y iIn x -> p y -> y iIn Sep x p claim !x:set.SNo x -> !y:set.SNo y -> SNoLev y iIn SNoLev x -> y < x -> y iIn SNoL x