for A being Element of LTLB_WFF holds nega <*A*> = <*('not' A)*>