theorem Th14: :: LTLAXIO3:14

for p, q being Element of LTLB_WFF holds tau1 . q c= tau1 . (p 'or' q)