theorem Th24: :: LTLAXIO3:24

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