const SNoCutP : set set prop const In : set set prop term iIn = In infix iIn 2000 2000 const SNoLt : set set prop term < = SNoLt infix < 2020 2020 const SNoCut : set set set const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 axiom SNoCut_Le: !x:set.!y:set.!z:set.!w:set.SNoCutP x y -> SNoCutP z w -> (!u:set.u iIn x -> u < SNoCut z w) -> (!u:set.u iIn w -> SNoCut x y < u) -> SNoCut x y <= SNoCut z w const SNo : set prop axiom SNoLe_antisym: !x:set.!y:set.SNo x -> SNo y -> x <= y -> y <= x -> x = y var x:set var y:set var z:set var w:set hyp SNoCutP x y hyp SNoCutP z w hyp !u:set.u iIn x -> u < SNoCut z w hyp !u:set.u iIn y -> SNoCut z w < u hyp !u:set.u iIn z -> u < SNoCut x y hyp !u:set.u iIn w -> SNoCut x y < u hyp SNo (SNoCut x y) claim SNo (SNoCut z w) -> SNoCut x y = SNoCut z w