let a be Data-Location ; :: thesis: not a in NAT
a in SCM-Data-Loc by AMI_3:def 2;
hence not a in NAT by AMI_2:29, XBOOLE_0:3; :: thesis: verum