:: deftheorem defines 'F' LTLAXIO1:def 7 :
for p being Element of LTLB_WFF holds 'F' p = 'not' ('G' ('not' p));