for A, B, p, q being Element of LTLB_WFF holds
( not p 'U' q in tau1 . (A '&&' B) or p 'U' q in tau1 . A or p 'U' q in tau1 . B )