set s = { ('G' A) where A is Element of LTLB_WFF : A in F } ;
{ ('G' A) where A is Element of LTLB_WFF : A in F } c= LTLB_WFF

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ('G' A) where A is Element of LTLB_WFF : A in F } or x in LTLB_WFF )
assume x in { ('G' A) where A is Element of LTLB_WFF : A in F } ; :: thesis: x in LTLB_WFF
then ex A being Element of LTLB_WFF st
( x = 'G' A & A in F ) ;
hence x in LTLB_WFF ; :: thesis: verum

end;

hence { ('G' A) where A is Element of LTLB_WFF : A in F } is Subset of LTLB_WFF ; :: thesis: verum