thus 'G' ({} LTLB_WFF) c= {} LTLB_WFF :: according to XBOOLE_0:def 10 :: thesis: {} LTLB_WFF c= 'G' ({} LTLB_WFF)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in 'G' ({} LTLB_WFF) or x in {} LTLB_WFF )
assume x in 'G' ({} LTLB_WFF) ; :: thesis: x in {} LTLB_WFF
then consider A being Element of LTLB_WFF such that
A1: ( x = 'G' A & A in {} LTLB_WFF ) ;
thus x in {} LTLB_WFF by A1; :: thesis: verum
end;
thus {} LTLB_WFF c= 'G' ({} LTLB_WFF) ; :: thesis: verum