for X being Subset of LTLB_WFF holds tau X = union { (tau1 . p) where p is Element of LTLB_WFF : p in X }