let i1, j1 be Nat; :: thesis: for G being Go-board st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G holds

for i2, j2 being Nat holds

( not 1 <= i2 or not i2 + 1 <= len G or not 1 <= j2 or not j2 <= width G or not (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) )

let G be Go-board; :: thesis: ( 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G implies for i2, j2 being Nat holds

( not 1 <= i2 or not i2 + 1 <= len G or not 1 <= j2 or not j2 <= width G or not (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) ) )

assume that

A1: ( 1 <= i1 & i1 <= len G ) and

A2: ( 1 <= j1 & j1 + 1 <= width G ) ; :: thesis: for i2, j2 being Nat holds

( not 1 <= i2 or not i2 + 1 <= len G or not 1 <= j2 or not j2 <= width G or not (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) )

A3: j1 < j1 + 1 by XREAL_1:29;

set mi = (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1))));

given i2, j2 being Nat such that A4: ( 1 <= i2 & i2 + 1 <= len G ) and

A5: ( 1 <= j2 & j2 <= width G ) and

A6: (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) ; :: thesis: contradiction

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;

then A9: LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) by A6, XBOOLE_0:3;

for i2, j2 being Nat holds

( not 1 <= i2 or not i2 + 1 <= len G or not 1 <= j2 or not j2 <= width G or not (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) )

let G be Go-board; :: thesis: ( 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G implies for i2, j2 being Nat holds

( not 1 <= i2 or not i2 + 1 <= len G or not 1 <= j2 or not j2 <= width G or not (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) ) )

assume that

A1: ( 1 <= i1 & i1 <= len G ) and

A2: ( 1 <= j1 & j1 + 1 <= width G ) ; :: thesis: for i2, j2 being Nat holds

( not 1 <= i2 or not i2 + 1 <= len G or not 1 <= j2 or not j2 <= width G or not (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) )

A3: j1 < j1 + 1 by XREAL_1:29;

set mi = (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1))));

given i2, j2 being Nat such that A4: ( 1 <= i2 & i2 + 1 <= len G ) and

A5: ( 1 <= j2 & j2 <= width G ) and

A6: (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) ; :: thesis: contradiction

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;

then A9: LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) by A6, XBOOLE_0:3;

per cases
( ( i1 = i2 & j1 = j2 ) or ( i1 = i2 & j1 + 1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 + 1 & j1 + 1 = j2 ) )
by A1, A2, A4, A5, A9, Th21;

end;

suppose A10:
( i1 = i2 & j1 = j2 )
; :: thesis: contradiction

then
(LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * ((i1 + 1),j1)),(G * (i1,j1)))) = {(G * (i1,j1))}
by A2, A4, Th17;

then (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in {(G * (i1,j1))} by A6, A8, A10, 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 A11: (1 / 2) * (G * (i1,(j1 + 1))) = (1 / 2) * (G * (i1,j1)) by Th3;

(G * (i1,(j1 + 1))) `2 > (G * (i1,j1)) `2 by A1, A2, A3, GOBOARD5:4;

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

end;then (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in {(G * (i1,j1))} by A6, A8, A10, 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 A11: (1 / 2) * (G * (i1,(j1 + 1))) = (1 / 2) * (G * (i1,j1)) by Th3;

(G * (i1,(j1 + 1))) `2 > (G * (i1,j1)) `2 by A1, A2, A3, GOBOARD5:4;

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

suppose A12:
( i1 = i2 & j1 + 1 = j2 )
; :: thesis: contradiction

then
(LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * ((i1 + 1),(j1 + 1))),(G * (i1,(j1 + 1))))) = {(G * (i1,(j1 + 1)))}
by A2, A4, Th15;

then (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in {(G * (i1,(j1 + 1)))} by A6, A8, A12, XBOOLE_0:def 4;

then ((1 / 2) * (G * (i1,j1))) + ((1 / 2) * (G * (i1,(j1 + 1)))) = G * (i1,(j1 + 1)) by A7, TARSKI:def 1

.= ((1 / 2) + (1 / 2)) * (G * (i1,(j1 + 1))) by RLVECT_1:def 8

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

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

(G * (i1,(j1 + 1))) `2 > (G * (i1,j1)) `2 by A1, A2, A3, GOBOARD5:4;

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

end;then (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in {(G * (i1,(j1 + 1)))} by A6, A8, A12, XBOOLE_0:def 4;

then ((1 / 2) * (G * (i1,j1))) + ((1 / 2) * (G * (i1,(j1 + 1)))) = G * (i1,(j1 + 1)) by A7, TARSKI:def 1

.= ((1 / 2) + (1 / 2)) * (G * (i1,(j1 + 1))) by RLVECT_1:def 8

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

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

(G * (i1,(j1 + 1))) `2 > (G * (i1,j1)) `2 by A1, A2, A3, GOBOARD5:4;

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

suppose A14:
( i1 = i2 + 1 & j1 = j2 )
; :: thesis: contradiction

then
(LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * (i1,j1)),(G * (i2,j1)))) = {(G * (i1,j1))}
by A2, A4, Th18;

then (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in {(G * (i1,j1))} by A6, A8, 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 A15: (1 / 2) * (G * (i1,(j1 + 1))) = (1 / 2) * (G * (i1,j1)) by Th3;

(G * (i1,(j1 + 1))) `2 > (G * (i1,j1)) `2 by A1, A2, A3, GOBOARD5:4;

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

end;then (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in {(G * (i1,j1))} by A6, A8, 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 A15: (1 / 2) * (G * (i1,(j1 + 1))) = (1 / 2) * (G * (i1,j1)) by Th3;

(G * (i1,(j1 + 1))) `2 > (G * (i1,j1)) `2 by A1, A2, A3, GOBOARD5:4;

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

suppose A16:
( i1 = i2 + 1 & j1 + 1 = j2 )
; :: thesis: contradiction

then
(LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) /\ (LSeg ((G * (i1,(j1 + 1))),(G * (i2,(j1 + 1))))) = {(G * (i1,(j1 + 1)))}
by A2, A4, Th16;

then (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in {(G * (i1,(j1 + 1)))} by A6, A8, A16, XBOOLE_0:def 4;

then ((1 / 2) * (G * (i1,j1))) + ((1 / 2) * (G * (i1,(j1 + 1)))) = G * (i1,(j1 + 1)) by A7, TARSKI:def 1

.= ((1 / 2) + (1 / 2)) * (G * (i1,(j1 + 1))) by RLVECT_1:def 8

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

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

(G * (i1,(j1 + 1))) `2 > (G * (i1,j1)) `2 by A1, A2, A3, GOBOARD5:4;

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

end;then (1 / 2) * ((G * (i1,j1)) + (G * (i1,(j1 + 1)))) in {(G * (i1,(j1 + 1)))} by A6, A8, A16, XBOOLE_0:def 4;

then ((1 / 2) * (G * (i1,j1))) + ((1 / 2) * (G * (i1,(j1 + 1)))) = G * (i1,(j1 + 1)) by A7, TARSKI:def 1

.= ((1 / 2) + (1 / 2)) * (G * (i1,(j1 + 1))) by RLVECT_1:def 8

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

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

(G * (i1,(j1 + 1))) `2 > (G * (i1,j1)) `2 by A1, A2, A3, GOBOARD5:4;

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