const SNo : set prop const Empty : set axiom SNo_0: SNo Empty const ordinal : set prop axiom ordinal_Empty: ordinal Empty const Subq : set set prop axiom Subq_Empty: !x:set.Subq Empty x const SNoLev : set set axiom ordinal_SNoLev: !x:set.ordinal x -> SNoLev x = x axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y const SNoEq_ : set set set prop axiom SNo_eq: !x:set.!y:set.SNo x -> SNo y -> SNoLev x = SNoLev y -> SNoEq_ (SNoLev x) x y -> x = y const SNoCut : set set set const binunion : set set set const Repl : set (set set) set const SNoL : set set const minus_SNo : set set term - = minus_SNo const add_SNo : set set set term + = add_SNo infix + 2281 2280 const SNoR : set set const SNoCutP : set set prop const In : set set prop term iIn = In infix iIn 2000 2000 const SNoS_ : set set var x:set hyp SNo x hyp !y:set.y iIn SNoS_ (SNoLev x) -> - y + y = Empty hyp SNo - x hyp SNoCutP (binunion (Repl (SNoL - x) \y:set.y + x) (Repl (SNoL x) (add_SNo - x))) (binunion (Repl (SNoR - x) \y:set.y + x) (Repl (SNoR x) (add_SNo - x))) hyp SNo (SNoCut (binunion (Repl (SNoL - x) \y:set.y + x) (Repl (SNoL x) (add_SNo - x))) (binunion (Repl (SNoR - x) \y:set.y + x) (Repl (SNoR x) (add_SNo - x)))) claim Subq (SNoLev (SNoCut (binunion (Repl (SNoL - x) \y:set.y + x) (Repl (SNoL x) (add_SNo - x))) (binunion (Repl (SNoR - x) \y:set.y + x) (Repl (SNoR x) (add_SNo - x))))) (SNoLev Empty) & SNoEq_ (SNoLev (SNoCut (binunion (Repl (SNoL - x) \y:set.y + x) (Repl (SNoL x) (add_SNo - x))) (binunion (Repl (SNoR - x) \y:set.y + x) (Repl (SNoR x) (add_SNo - x))))) (SNoCut (binunion (Repl (SNoL - x) \y:set.y + x) (Repl (SNoL x) (add_SNo - x))) (binunion (Repl (SNoR - x) \y:set.y + x) (Repl (SNoR x) (add_SNo - x)))) Empty -> SNoCut (binunion (Repl (SNoL - x) \y:set.y + x) (Repl (SNoL x) (add_SNo - x))) (binunion (Repl (SNoR - x) \y:set.y + x) (Repl (SNoR x) (add_SNo - x))) = Empty