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