assume not LocNums F,S is empty ; :: thesis: contradiction
then consider x being set such that
A1: x in LocNums F,S by XBOOLE_0:def 1;
ex l being Element of NAT st
( x = locnum l,S & l in F ) by A1;
hence contradiction ; :: thesis: verum