theorem :: LTLAXIO2:16

for f, f1 being FinSequence of LTLB_WFF holds nega (f ^ f1) = (nega f) ^ (nega f1)