let a be Data-Location ; :: thesis: not a in NAT
a in SCM-Data-Loc by Def2;
hence not a in NAT by AMI_2:21, XBOOLE_0:3; :: thesis: verum