:: deftheorem Def5 defines nex LTLAXIO2:def 5 :
for f, b₂ being FinSequence of LTLB_WFF holds
( b₂ = nex f iff ( len b₂ = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b₂ . i = 'X' (f /. i) ) ) );