theorem Th9: :: SCMPDS_3:10

for s being State of SCMPDS holds (IC s) + 1 = ICplusConst (s,1)