theorem :: LTLAXIO3:17

for X being Subset of LTLB_WFF holds tau (tau X) = tau X