:: deftheorem Def4 defines nega LTLAXIO2:def 4 :
for f, b₂ being FinSequence of LTLB_WFF holds
( b₂ = nega f iff ( len b₂ = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b₂ . i = 'not' (f /. i) ) ) );