:: deftheorem defines alternating SPPOL_1:def 4 :
for IT being FinSequence of (TOP-REAL 2) holds
( IT is alternating iff for i being Nat st 1 <= i & i + 2 <= len IT holds
( (IT /. i) `1 <> (IT /. (i + 2)) `1 & (IT /. i) `2 <> (IT /. (i + 2)) `2 ) );