theorem Th4: :: SCMPDS_6:12

for s being State of SCMPDS
for m1, m2 being Nat st IC s = m1 holds
ICplusConst (s,m2) = m1 + m2