for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds
( F |= A iff 'G' F |=0 A )