let i1, j1, i2, j2 be Element of NAT ; :: thesis: for G being Go-board st 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in LSeg (G * i2,j2),(G * (i2 + 1),j2) holds
( i1 = i2 & j1 = j2 )
let G be Go-board; :: thesis: ( 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in LSeg (G * i2,j2),(G * (i2 + 1),j2) implies ( i1 = i2 & j1 = j2 ) )
assume that
A1: 1 <= i1 and
A2: i1 + 1 <= len G and
A3: ( 1 <= j1 & j1 <= width G ) and
A4: 1 <= i2 and
A5: i2 + 1 <= len G and
A6: ( 1 <= j2 & j2 <= width G ) ; :: thesis: ( not (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in LSeg (G * i2,j2),(G * (i2 + 1),j2) or ( i1 = i2 & j1 = j2 ) )
set mi = (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1));
A7: ((1 / 2) * (G * i1,j1)) + ((1 / 2) * (G * (i1 + 1),j1)) = (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) by EUCLID:36;
then A8: (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in LSeg (G * i1,j1),(G * (i1 + 1),j1) by Lm1;
assume A9: (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in LSeg (G * i2,j2),(G * (i2 + 1),j2) ; :: thesis: ( i1 = i2 & j1 = j2 )
then A10: LSeg (G * i1,j1),(G * (i1 + 1),j1) meets LSeg (G * i2,j2),(G * (i2 + 1),j2) by A8, XBOOLE_0:3;
then A11: j1 = j2 by A1, A2, A3, A4, A5, A6, Th22;

now

i1 < i1 + 1 by XREAL_1:31;
then A12: (G * (i1 + 1),j1) `1 > (G * i1,j1) `1 by A1, A2, A3, GOBOARD5:4;
assume A13: abs (i1 - i2) = 1 ; :: thesis: contradiction

per cases ( i1 = i2 + 1 or i1 + 1 = i2 ) by A13, GOBOARD1:1;

suppose A14: i1 = i2 + 1 ; :: thesis: contradiction

then (LSeg (G * i2,j2),(G * (i2 + 1),j2)) /\ (LSeg (G * (i2 + 1),j2),(G * (i2 + 2),j2)) = {(G * (i2 + 1),j2)} by A2, A4, A6, Th16;
then (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in {(G * i1,j1)} by A9, A8, A11, A14, XBOOLE_0:def 4;
then ((1 / 2) * (G * i1,j1)) + ((1 / 2) * (G * (i1 + 1),j1)) = G * i1,j1 by A7, TARSKI:def 1
.= ((1 / 2) + (1 / 2)) * (G * i1,j1) by EUCLID:33
.= ((1 / 2) * (G * i1,j1)) + ((1 / 2) * (G * i1,j1)) by EUCLID:37 ;
then (1 / 2) * (G * i1,j1) = (1 / 2) * (G * (i1 + 1),j1) by Th3;
hence contradiction by A12, EUCLID:38; :: thesis: verum

end;

suppose A15: i1 + 1 = i2 ; :: thesis: contradiction

then (LSeg (G * i1,j2),(G * (i1 + 1),j2)) /\ (LSeg (G * (i1 + 1),j2),(G * (i1 + 2),j2)) = {(G * (i1 + 1),j2)} by A1, A5, A6, Th16;
then (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in {(G * i2,j1)} by A9, A8, A11, A15, XBOOLE_0:def 4;
then ((1 / 2) * (G * i1,j1)) + ((1 / 2) * (G * (i1 + 1),j1)) = G * i2,j1 by A7, TARSKI:def 1
.= ((1 / 2) + (1 / 2)) * (G * i2,j1) by EUCLID:33
.= ((1 / 2) * (G * i2,j1)) + ((1 / 2) * (G * i2,j1)) by EUCLID:37 ;
then (1 / 2) * (G * i1,j1) = (1 / 2) * (G * (i1 + 1),j1) by A15, Th3;
hence contradiction by A12, EUCLID:38; :: thesis: verum

end;

end;

end;

then abs (i1 - i2) = 0 by A1, A2, A3, A4, A5, A6, A10, Th22, NAT_1:26;
hence i1 = i2 by Th2; :: thesis: j1 = j2
thus j1 = j2 by A1, A2, A3, A4, A5, A6, A10, Th22; :: thesis: verum