theorem :: LTLAXIO3:26

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