for i being Nat
for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `2 = (f /. (i + 1)) `2 holds
(f /. (i + 1)) `1 = (f /. (i + 2)) `1