:: deftheorem defines 'G' LTLAXIO1:def 6 :
for p being Element of LTLB_WFF holds 'G' p = 'not' (('not' p) 'or' (TVERUM 'U' ('not' p)));