let I be Program of SCMPDS ; :: thesis: not IC SCMPDS in dom I
assume A1: IC SCMPDS in dom I ; :: thesis: contradiction
dom I c= NAT by RELAT_1:def 18;
then reconsider l = IC SCMPDS as Instruction-Location of SCMPDS by A1, AMI_1:def 4;
l = IC SCMPDS ;
hence contradiction by AMI_1:48; :: thesis: verum