theorem :: LTLAXIO2:14

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