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