:: deftheorem Def24 defines axltl2 LTLAXIO1:def 24 :
for A being Element of LTLB_WFF holds
( A is axltl2 iff ex B, C being Element of LTLB_WFF st A = ('X' (B => C)) => (('X' B) => ('X' C)) );