theorem Th3: :: JORDAN8:3

for k being Nat
for D being set
for f being FinSequence of D
for G being Matrix of D st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
ex i1, j1, i2, j2 being Nat st
( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) )