let s be State of SCMPDS ; :: thesis: for m, n being Element of NAT st IC s = m holds
ICplusConst s,(n - m) = n
let m, n be Element of NAT ; :: thesis: ( IC s = m implies ICplusConst s,(n - m) = n )
consider k being Element of NAT such that
A1: k = IC s and
A2: ICplusConst s,(n - m) = abs (k + (n - m)) by SCMPDS_2:def 20;
assume IC s = m ; :: thesis: ICplusConst s,(n - m) = n
then k = m by A1
.= m ;
hence ICplusConst s,(n - m) = n by A2, ABSVALUE:def 1
.= n ;
:: thesis: verum