theorem :: SCMPDS_4:6

for s being State of SCMPDS
for x being set holds
( not x in dom s or x is Int_position or x = IC )