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 or x is Element of NAT )
let x be set ; :: thesis: ( not x in dom s or x is Int_position or x = IC or x is Element of NAT )
assume A1: x in dom s ; :: thesis: ( x is Int_position or x = IC or x is Element of NAT )
dom s = the carrier of SCMPDS by PARTFUN1:def 4;
then dom s = ({(IC )} \/ SCM-Data-Loc) \/ NAT by COMPOS_1:160, SCMPDS_2:100;
then ( x in {(IC )} \/ SCM-Data-Loc or x in NAT ) by A1, XBOOLE_0:def 3;
then ( x in {(IC )} or x in SCM-Data-Loc or x in NAT ) by XBOOLE_0:def 3;
hence ( x is Int_position or x = IC or x is Element of NAT ) by SCMPDS_2:9, TARSKI:def 1; :: thesis: verum