:: deftheorem Def28 defines axltl6 LTLAXIO1:def 28 :
for A being Element of LTLB_WFF holds
( A is axltl6 iff ex B, C being Element of LTLB_WFF st A = (B 'U' C) => ('X' ('F' C)) );