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