let i be Instruction-Location of SCMPDS ; :: thesis: not i in SCM-Data-Loc
i in NAT by AMI_1:def 4;
hence not i in SCM-Data-Loc by AMI_2:29, XBOOLE_0:3; :: thesis: verum