:: deftheorem Def22 defines axltl1 LTLAXIO1:def 22 :
for A being Element of LTLB_WFF holds
( A is axltl1 iff ex B being Element of LTLB_WFF st A = ('not' ('X' B)) => ('X' ('not' B)) );