let l be Instruction-Location of SCM ; :: thesis: l is natural
l in NAT by AMI_1:def 4;
hence l is natural ; :: thesis: verum