theorem Th9: :: SCMPDS_3:10
for s being State of SCMPDS holds (IC s) + 1 = ICplusConst (s,1)