let a be Int-Location ; :: thesis: not a in NAT
a in SCM+FSA-Data-Loc by SCMFSA_2:def 4;
hence not a in NAT by SCMFSA_2:13, XBOOLE_0:3; :: thesis: verum