let i1, i2, j1, j2 be Nat; :: thesis: 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 )
let G be Go-board; :: thesis: ( 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)))) implies ( i1 = i2 & j1 = j2 ) )
assume that
A1: ( 1 <= i1 & i1 <= len G ) and
A2: 1 <= j1 and
A3: j1 + 1 <= width G and
A4: ( 1 <= i2 & i2 <= len G ) and
A5: 1 <= j2 and
A6: j2 + 1 <= width G ; :: thesis: ( not (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1)))) or ( i1 = i2 & j1 = j2 ) )
set mi = (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1))));
A7: ((1 / 2) * (G * (i1,j1))) + ((1 / 2) * (G * (i1,(j1 + 1)))) = (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) by RLVECT_1:def 5;
then A8: (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) by Lm1;
assume A9: (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1)))) ; :: thesis: ( i1 = i2 & j1 = j2 )
then A10: LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) meets LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1)))) by A8, XBOOLE_0:3;
hence A11: i1 = i2 by A1, A2, A3, A4, A5, A6, Th19; :: thesis: j1 = j2

now :: thesis: not |.(j1 - j2).| = 1

j1 < j1 + 1 by XREAL_1:29;
then A12: (G * (i1,(j1 + 1))) `2 > (G * (i1,j1)) `2 by A1, A2, A3, GOBOARD5:4;
assume A13: |.(j1 - j2).| = 1 ; :: thesis: contradiction

per cases ( j1 = j2 + 1 or j1 + 1 = j2 ) by A13, SEQM_3:41;

suppose A14: j1 = j2 + 1 ; :: thesis: contradiction

then (LSeg ((G * (i2,j2)),(G * (i2,(j2 + 1))))) /\ (LSeg ((G * (i2,(j2 + 1))),(G * (i2,(j2 + 2))))) = {(G * (i2,(j2 + 1)))} by A3, A4, A5, Th13;
then (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in {(G * (i1,j1))} by A9, A8, A11, A14, XBOOLE_0:def 4;
then ((1 / 2) * (G * (i1,j1))) + ((1 / 2) * (G * (i1,(j1 + 1)))) = G * (i1,j1) by A7, TARSKI:def 1
.= ((1 / 2) + (1 / 2)) * (G * (i1,j1)) by RLVECT_1:def 8
.= ((1 / 2) * (G * (i1,j1))) + ((1 / 2) * (G * (i1,j1))) by RLVECT_1:def 6 ;
then (1 / 2) * (G * (i1,j1)) = (1 / 2) * (G * (i1,(j1 + 1))) by Th3;
hence contradiction by A12, RLVECT_1:36; :: thesis: verum

end;

suppose A15: j1 + 1 = j2 ; :: thesis: contradiction

then (LSeg ((G * (i2,j1)),(G * (i2,(j1 + 1))))) /\ (LSeg ((G * (i2,(j1 + 1))),(G * (i2,(j1 + 2))))) = {(G * (i2,(j1 + 1)))} by A2, A4, A6, Th13;
then (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in {(G * (i1,j2))} by A9, A8, A11, A15, XBOOLE_0:def 4;
then ((1 / 2) * (G * (i1,j1))) + ((1 / 2) * (G * (i1,(j1 + 1)))) = G * (i1,j2) by A7, TARSKI:def 1
.= ((1 / 2) + (1 / 2)) * (G * (i1,j2)) by RLVECT_1:def 8
.= ((1 / 2) * (G * (i1,j2))) + ((1 / 2) * (G * (i1,j2))) by RLVECT_1:def 6 ;
then (1 / 2) * (G * (i1,j1)) = (1 / 2) * (G * (i1,(j1 + 1))) by A15, Th3;
hence contradiction by A12, RLVECT_1:36; :: thesis: verum

end;

end;

end;

then |.(j1 - j2).| = 0 by A1, A2, A3, A4, A5, A6, A10, Th19, NAT_1:25;
hence j1 = j2 by Th2; :: thesis: verum