theorem Th6: :: LTLAXIO3:6

for p being Element of LTLB_WFF holds p in tau1 . p