:: deftheorem defines 'Uw' LTLAXIO1:def 8 :
for p, q being Element of LTLB_WFF holds p 'Uw' q = q 'or' (p '&&' (p 'U' q));