:: deftheorem defines untn LTLAXIO2:def 1 :
for A, B being Element of LTLB_WFF holds untn (A,B) = B 'or' (A '&&' (A 'U' B));