const SNo : set prop const Subq : set set prop const SNoLev : set set const minus_SNo : set set term - = minus_SNo axiom minus_SNo_Lev_lem2: !x:set.SNo x -> Subq (SNoLev - x) (SNoLev x) axiom SNo_minus_SNo: !x:set.SNo x -> SNo - x axiom minus_SNo_invol: !x:set.SNo x -> - - x = x axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y claim !x:set.SNo x -> SNoLev - x = SNoLev x