let s be State of ; :: thesis: for m1, m2 being Element of NAT st IC s = inspos (m1 + m2) holds
ICplusConst s,(- m2) = inspos m1
let m1, m2 be Element of NAT ; :: thesis: ( IC s = inspos (m1 + m2) implies ICplusConst s,(- m2) = inspos m1 )
assume A1: IC s = inspos (m1 + m2) ; :: thesis: ICplusConst s,(- m2) = inspos m1
consider m being Element of NAT such that
A2: m = IC s and
A3: ICplusConst s,(- m2) = abs (m + (- m2)) by SCMPDS_2:def 20;
A4: m = il. (m1 + m2) by A1, A2
.= m1 + m2 ;
m1 >= 0 by NAT_1:2;
hence ICplusConst s,(- m2) = m1 by A3, A4, ABSVALUE:def 1
.= il. m1
.= inspos m1 ;
:: thesis: verum