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

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

proof

hence
{ ('G' A) where A is Element of LTLB_WFF : A in F } is Subset of LTLB_WFF
; :: thesis: verum
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;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