:: deftheorem defines 'G' LTLAXIO5:def 4 :
for F being Subset of LTLB_WFF holds 'G' F = { ('G' A) where A is Element of LTLB_WFF : A in F } ;