const In : set set prop term iIn = In infix iIn 2000 2000 const SNo : set prop const SNo_max_of : set set prop const SNo_min_of : set set prop const Repl : set (set set) set const minus_SNo : set set term - = minus_SNo axiom minus_SNo_max_min: !x:set.!y:set.(!z:set.z iIn x -> SNo z) -> SNo_max_of x y -> SNo_min_of (Repl x minus_SNo) - y var x:set var y:set hyp !z:set.z iIn x -> SNo z hyp SNo_max_of (Repl x minus_SNo) y hyp Repl (Repl x minus_SNo) minus_SNo = x claim (!z:set.z iIn Repl x minus_SNo -> SNo z) -> SNo_min_of x - y