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