set A = { (locnum l,S) where l is Element of NAT : l in F } ;
{ (locnum l,S) where l is Element of NAT : l in F } c= NAT

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (locnum l,S) where l is Element of NAT : l in F } or a in NAT )
assume a in { (locnum l,S) where l is Element of NAT : l in F } ; :: thesis: a in NAT
then ex l being Element of NAT st
( a = locnum l,S & l in F ) ;
hence a in NAT ; :: thesis: verum

end;

hence { (locnum l,S) where l is Element of NAT : l in F } is Subset of NAT ; :: thesis: verum