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