theorem :: AMI_2:26

for k being Element of SCM-Memory holds
( k = NAT or k in SCM-Data-Loc ) by Lm1;