for A being Element of LTLB_WFF holds [(<*> LTLB_WFF),<*A*>] ^ = TVERUM '&&' ('not' A)