set S1 = {(IC )};
set S2 = SCM-Data-Loc ;
set S3 = NAT ;
let s be State of SCMPDS; :: thesis: for x being set holds
( not x in dom s or x is Int_position or x = IC )
let x be set ; :: thesis: ( not x in dom s or x is Int_position or x = IC )
assume A1: x in dom s ; :: thesis: ( x is Int_position or x = IC )
dom s = the carrier of SCMPDS by PARTFUN1:def 2;
then x in {(IC )} \/ SCM-Data-Loc by A1, SCMPDS_2:84, STRUCT_0:4;
then ( x in {(IC )} or x in SCM-Data-Loc ) by XBOOLE_0:def 3;
hence ( x is Int_position or x = IC ) by AMI_2:def 16, TARSKI:def 1; :: thesis: verum