theorem :: LTLAXIO3:18

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