const binunion : set set set const Sep : set (set prop) set const ReplSep : set (set prop) (set set) set const SetAdjoin : set set set const Sing : set set const ordsucc : set set const Empty : set term PSNo = \x:set.\p:set prop.binunion (Sep x p) (ReplSep x (\y:set.~ p y) \y:set.SetAdjoin y (Sing (ordsucc Empty))) const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y const SNoLev : set set term SNo_extend0 = \x:set.PSNo (ordsucc (SNoLev x)) \y:set.y iIn x & y != SNoLev x axiom SepE2: !x:set.!p:set prop.!y:set.y iIn Sep x p -> p y const SNo : set prop const ordinal : set prop axiom SNoLev_ordinal: !x:set.SNo x -> ordinal (SNoLev x) axiom tagged_not_ordinal: !x:set.~ ordinal (SetAdjoin x (Sing (ordsucc Empty))) axiom ReplSepE_impred: !x:set.!p:set prop.!f:set set.!y:set.y iIn ReplSep x p f -> !P:prop.(!z:set.z iIn x -> p z -> y = f z -> P) -> P axiom binunionE: !x:set.!y:set.!z:set.z iIn binunion x y -> z iIn x | z iIn y claim !x:set.SNo x -> ~ SNoLev x iIn SNo_extend0 x