consider l being Element of NAT such that
A1: l in F by SUBSET_1:10;
reconsider l = l as Instruction-Location of S by AMI_1:def 4;
l in F by A1;
hence not LocNums F is empty by Th25; :: thesis: verum