let i1, j1 be Element of NAT ; :: thesis: for G being Go-board st 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G holds
for i2, j2 being Element of NAT holds
( not 1 <= i2 or not i2 <= len G or not 1 <= j2 or not j2 + 1 <= width G or not (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in LSeg (G * i2,j2),(G * i2,(j2 + 1)) )
let G be Go-board; :: thesis: ( 1 <= i1 & i1 + 1 <= len G & 1 <= j1 & j1 <= width G implies for i2, j2 being Element of NAT holds
( not 1 <= i2 or not i2 <= len G or not 1 <= j2 or not j2 + 1 <= width G or not (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in LSeg (G * i2,j2),(G * i2,(j2 + 1)) ) )
assume that
A1: ( 1 <= i1 & i1 + 1 <= len G ) and
A2: ( 1 <= j1 & j1 <= width G ) ; :: thesis: for i2, j2 being Element of NAT holds
( not 1 <= i2 or not i2 <= len G or not 1 <= j2 or not j2 + 1 <= width G or not (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in LSeg (G * i2,j2),(G * i2,(j2 + 1)) )
set mi = (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1));
given i2, j2 being Element of NAT such that A3: ( 1 <= i2 & i2 <= len G ) and
A4: ( 1 <= j2 & j2 + 1 <= width G ) and
A5: (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in LSeg (G * i2,j2),(G * i2,(j2 + 1)) ; :: thesis: contradiction
A6: i1 < i1 + 1 by XREAL_1:31;
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;
then A9: LSeg (G * i1,j1),(G * (i1 + 1),j1) meets LSeg (G * i2,j2),(G * i2,(j2 + 1)) by A5, XBOOLE_0:3;

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

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

then (LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * i1,(j1 + 1)),(G * i1,j1)) = {(G * i1,j1)} by A1, A4, Th19;
then (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in {(G * i1,j1)} by A5, A8, A10, 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 A11: (1 / 2) * (G * (i1 + 1),j1) = (1 / 2) * (G * i1,j1) by Th3;
(G * (i1 + 1),j1) `1 > (G * i1,j1) `1 by A1, A2, A6, GOBOARD5:4;
hence contradiction by A11, EUCLID:38; :: thesis: verum

end;

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

then (LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * (i1 + 1),(j1 + 1)),(G * (i1 + 1),j1)) = {(G * (i1 + 1),j1)} by A1, A4, Th20;
then (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in {(G * (i1 + 1),j1)} by A5, A8, A12, XBOOLE_0:def 4;
then ((1 / 2) * (G * i1,j1)) + ((1 / 2) * (G * (i1 + 1),j1)) = G * (i1 + 1),j1 by A7, TARSKI:def 1
.= ((1 / 2) + (1 / 2)) * (G * (i1 + 1),j1) by EUCLID:33
.= ((1 / 2) * (G * (i1 + 1),j1)) + ((1 / 2) * (G * (i1 + 1),j1)) by EUCLID:37 ;
then A13: (1 / 2) * (G * (i1 + 1),j1) = (1 / 2) * (G * i1,j1) by Th3;
(G * (i1 + 1),j1) `1 > (G * i1,j1) `1 by A1, A2, A6, GOBOARD5:4;
hence contradiction by A13, EUCLID:38; :: thesis: verum

end;

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

then (LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * i1,j1),(G * i1,j2)) = {(G * i1,j1)} by A1, A4, Th17;
then (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in {(G * i1,j1)} by A5, A8, 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 A15: (1 / 2) * (G * (i1 + 1),j1) = (1 / 2) * (G * i1,j1) by Th3;
(G * (i1 + 1),j1) `1 > (G * i1,j1) `1 by A1, A2, A6, GOBOARD5:4;
hence contradiction by A15, EUCLID:38; :: thesis: verum

end;

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

then (LSeg (G * i1,j1),(G * (i1 + 1),j1)) /\ (LSeg (G * (i1 + 1),j1),(G * (i1 + 1),j2)) = {(G * (i1 + 1),j1)} by A1, A4, Th18;
then (1 / 2) * ((G * i1,j1) + (G * (i1 + 1),j1)) in {(G * (i1 + 1),j1)} by A5, A8, A16, XBOOLE_0:def 4;
then ((1 / 2) * (G * i1,j1)) + ((1 / 2) * (G * (i1 + 1),j1)) = G * (i1 + 1),j1 by A7, TARSKI:def 1
.= ((1 / 2) + (1 / 2)) * (G * (i1 + 1),j1) by EUCLID:33
.= ((1 / 2) * (G * (i1 + 1),j1)) + ((1 / 2) * (G * (i1 + 1),j1)) by EUCLID:37 ;
then A17: (1 / 2) * (G * (i1 + 1),j1) = (1 / 2) * (G * i1,j1) by Th3;
(G * (i1 + 1),j1) `1 > (G * i1,j1) `1 by A1, A2, A6, GOBOARD5:4;
hence contradiction by A17, EUCLID:38; :: thesis: verum

end;

end;