theorem Th26: :: JORDAN1H:26
for i1, j1, i2, j2 being Nat
for G being Go-board st [i1,j1] in Indices G & [i2,j2] in Indices G & G * (i1,j1) = G * (i2,j2) holds
( i1 = i2 & j1 = j2 )