theorem Th16: :: LTLAXIO3:16

for X being Subset of LTLB_WFF holds X c= tau X