const SNoCutP : set set prop const SNo : set prop const SNoCut : set set set axiom SNoCutP_SNo_SNoCut: !x:set.!y:set.SNoCutP x y -> SNo (SNoCut x y) const minus_SNo : set set term - = minus_SNo const Repl : set (set set) set axiom minus_SNoCut_eq_lem: !x:set.SNo x -> !y:set.!z:set.SNoCutP y z -> x = SNoCut y z -> - x = SNoCut (Repl z minus_SNo) (Repl y minus_SNo) claim !x:set.!y:set.SNoCutP x y -> - SNoCut x y = SNoCut (Repl y minus_SNo) (Repl x minus_SNo)