for p, q being Element of LTLB_WFF holds p 'U' q in Sub . (p 'U' q)