let l be Instruction-Location of S; :: thesis: l is natural
l in NAT by Def4;
hence l is natural ; :: thesis: verum