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