let s be State of ; :: thesis: for m, n being Element of NAT st IC s = inspos m holds
ICplusConst s,(n - m) = inspos n
let m, n be Element of NAT ; :: thesis: ( IC s = inspos m implies ICplusConst s,(n - m) = inspos 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 = inspos m ; :: thesis: ICplusConst s,(n - m) = inspos n
then k = il. m by A1
.= m ;
hence ICplusConst s,(n - m) = il. n by A2, ABSVALUE:def 1
.= inspos n ;
:: thesis: verum