:: deftheorem Def25 defines axltl3 LTLAXIO1:def 25 :
for A being Element of LTLB_WFF holds
( A is axltl3 iff ex B being Element of LTLB_WFF st A = ('G' B) => (B '&&' ('X' ('G' B))) );