theorem :: JORDAN8:6

for G being Go-board

for p being Point of (TOP-REAL 2)

for f being non empty FinSequence of (TOP-REAL 2) st f is_sequence_on G & ex i, j being Nat st

( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. (len f) = G * (i1,j1) & p = G * (i2,j2) holds

|.(i2 - i1).| + |.(j2 - j1).| = 1 ) holds

f ^ <*p*> is_sequence_on G

for p being Point of (TOP-REAL 2)

for f being non empty FinSequence of (TOP-REAL 2) st f is_sequence_on G & ex i, j being Nat st

( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & f /. (len f) = G * (i1,j1) & p = G * (i2,j2) holds

|.(i2 - i1).| + |.(j2 - j1).| = 1 ) holds

f ^ <*p*> is_sequence_on G