theorem Th8: :: LTLAXIO3:8

for p, q being Element of LTLB_WFF st p in tau1 . q holds
tau1 . p c= tau1 . q