theorem Th25: :: GOBOARD7:25

for i1, i2, j1, j2 being Nat
for G being Go-board st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 <= len G & 1 <= j2 & j2 + 1 <= width G & (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1)))) holds
( i1 = i2 & j1 = j2 )