theorem :: AMI_2:23

for x being set st x in SCM-Data-Loc holds
ex k being Nat st x = [1,k]