theorem :: LTLAXIO2:15

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