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