for X being Subset of LTLB_WFF st X is without_implication holds
tau X = X