:: deftheorem Def4 defines Alternating GRAPH_2:def 4 :
for f being FinSequence holds
( f is Alternating iff for i being Nat st 1 <= i & i + 1 <= len f holds
f . i <> f . (i + 1) );