let i1, i2, j1, j2 be 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 RLVECT_1:def 5;

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, Th20;

hence i1 = i2 by Th2; :: thesis: j1 = j2

thus j1 = j2 by A1, A2, A3, A4, A5, A6, A10, Th20; :: thesis: verum

( 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 RLVECT_1:def 5;

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, Th20;

now :: thesis: not |.(i1 - i2).| = 1

then
|.(i1 - i2).| = 0
by A1, A2, A3, A4, A5, A6, A10, Th20, NAT_1:25;
i1 < i1 + 1
by XREAL_1:29;

then A12: (G * ((i1 + 1),j1)) `1 > (G * (i1,j1)) `1 by A1, A2, A3, GOBOARD5:3;

assume A13: |.(i1 - i2).| = 1 ; :: thesis: contradiction

end;then A12: (G * ((i1 + 1),j1)) `1 > (G * (i1,j1)) `1 by A1, A2, A3, GOBOARD5:3;

assume A13: |.(i1 - i2).| = 1 ; :: thesis: contradiction

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

end;

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, Th14;

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 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 + 1),j1)) by Th3;

hence contradiction by A12, RLVECT_1:36; :: thesis: verum

end;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 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 + 1),j1)) by Th3;

hence contradiction by A12, RLVECT_1:36; :: thesis: verum

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, Th14;

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 RLVECT_1:def 8

.= ((1 / 2) * (G * (i2,j1))) + ((1 / 2) * (G * (i2,j1))) by RLVECT_1:def 6 ;

then (1 / 2) * (G * (i1,j1)) = (1 / 2) * (G * ((i1 + 1),j1)) by A15, Th3;

hence contradiction by A12, RLVECT_1:36; :: thesis: verum

end;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 RLVECT_1:def 8

.= ((1 / 2) * (G * (i2,j1))) + ((1 / 2) * (G * (i2,j1))) by RLVECT_1:def 6 ;

then (1 / 2) * (G * (i1,j1)) = (1 / 2) * (G * ((i1 + 1),j1)) by A15, Th3;

hence contradiction by A12, RLVECT_1:36; :: thesis: verum

hence i1 = i2 by Th2; :: thesis: j1 = j2

thus j1 = j2 by A1, A2, A3, A4, A5, A6, A10, Th20; :: thesis: verum