:: deftheorem Def27 defines axltl5 LTLAXIO1:def 27 :
for A being Element of LTLB_WFF holds
( A is axltl5 iff ex B, C being Element of LTLB_WFF st A = (('X' C) 'or' ('X' (B '&&' (B 'U' C)))) => (B 'U' C) );