let G be Go-board; :: thesis: for i1, j1, i2, j2 being Element of NAT st 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 <= len G & 1 <= j2 & j2 + 1 <= width G & LSeg (G * i1,j1),(G * i1,(j1 + 1)) meets LSeg (G * i2,j2),(G * i2,(j2 + 1)) holds
( i1 = i2 & abs (j1 - j2) <= 1 )
let i1, j1, i2, j2 be Element of NAT ; :: thesis: ( 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 <= len G & 1 <= j2 & j2 + 1 <= width G & LSeg (G * i1,j1),(G * i1,(j1 + 1)) meets LSeg (G * i2,j2),(G * i2,(j2 + 1)) implies ( i1 = i2 & abs (j1 - j2) <= 1 ) )
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 LSeg (G * i1,j1),(G * i1,(j1 + 1)) meets LSeg (G * i2,j2),(G * i2,(j2 + 1)) or ( i1 = i2 & abs (j1 - j2) <= 1 ) )
A7: 1 <= j1 + 1 by A2, NAT_1:13;
A8: j1 < width G by A3, NAT_1:13;
assume LSeg (G * i1,j1),(G * i1,(j1 + 1)) meets LSeg (G * i2,j2),(G * i2,(j2 + 1)) ; :: thesis: ( i1 = i2 & abs (j1 - j2) <= 1 )
then consider x being set such that
A9: x in LSeg (G * i1,j1),(G * i1,(j1 + 1)) and
A10: x in LSeg (G * i2,j2),(G * i2,(j2 + 1)) by XBOOLE_0:3;
reconsider p = x as Point of (TOP-REAL 2) by A9;
consider r1 being Real such that
A11: p = ((1 - r1) * (G * i1,j1)) + (r1 * (G * i1,(j1 + 1))) and
A12: r1 >= 0 and
A13: r1 <= 1 by A9;
consider r2 being Real such that
A14: p = ((1 - r2) * (G * i2,j2)) + (r2 * (G * i2,(j2 + 1))) and
A15: r2 >= 0 and
A16: r2 <= 1 by A10;
A17: 1 <= j2 + 1 by A5, NAT_1:13;
A18: j2 < width G by A6, NAT_1:13;
assume A19: ( not i1 = i2 or not abs (j1 - j2) <= 1 ) ; :: thesis: contradiction

per cases ( i1 <> i2 or abs (j1 - j2) > 1 ) by A19;

suppose i1 <> i2 ; :: thesis: contradiction

then A20: ( i1 < i2 or i2 < i1 ) by XXREAL_0:1;
A21: (G * i2,j2) `1 = (G * i2,1) `1 by A4, A5, A18, GOBOARD5:3
.= (G * i2,(j2 + 1)) `1 by A4, A6, A17, GOBOARD5:3 ;
(G * i1,j1) `1 = (G * i1,1) `1 by A1, A2, A8, GOBOARD5:3
.= (G * i1,(j1 + 1)) `1 by A1, A3, A7, GOBOARD5:3 ;
then 1 * ((G * i1,j1) `1 ) = ((1 - r1) * ((G * i1,j1) `1 )) + (r1 * ((G * i1,(j1 + 1)) `1 ))
.= (((1 - r1) * (G * i1,j1)) `1 ) + (r1 * ((G * i1,(j1 + 1)) `1 )) by TOPREAL3:9
.= (((1 - r1) * (G * i1,j1)) `1 ) + ((r1 * (G * i1,(j1 + 1))) `1 ) by TOPREAL3:9
.= p `1 by A11, TOPREAL3:7
.= (((1 - r2) * (G * i2,j2)) `1 ) + ((r2 * (G * i2,(j2 + 1))) `1 ) by A14, TOPREAL3:7
.= ((1 - r2) * ((G * i2,j2) `1 )) + ((r2 * (G * i2,(j2 + 1))) `1 ) by TOPREAL3:9
.= ((1 - r2) * ((G * i2,j2) `1 )) + (r2 * ((G * i2,(j2 + 1)) `1 )) by TOPREAL3:9
.= (G * i2,1) `1 by A4, A6, A17, A21, GOBOARD5:3
.= (G * i2,j1) `1 by A2, A4, A8, GOBOARD5:3 ;
hence contradiction by A1, A2, A4, A8, A20, GOBOARD5:4; :: thesis: verum

end;

suppose A22: abs (j1 - j2) > 1 ; :: thesis: contradiction

A23: (G * i2,(j2 + 1)) `2 = (G * 1,(j2 + 1)) `2 by A4, A6, A17, GOBOARD5:2
.= (G * i1,(j2 + 1)) `2 by A1, A6, A17, GOBOARD5:2 ;
A24: (G * i2,j2) `2 = (G * 1,j2) `2 by A4, A5, A18, GOBOARD5:2
.= (G * i1,j2) `2 by A1, A5, A18, GOBOARD5:2 ;
A25: ((1 - r1) * ((G * i1,j1) `2 )) + (r1 * ((G * i1,(j1 + 1)) `2 )) = (((1 - r1) * (G * i1,j1)) `2 ) + (r1 * ((G * i1,(j1 + 1)) `2 )) by TOPREAL3:9
.= (((1 - r1) * (G * i1,j1)) `2 ) + ((r1 * (G * i1,(j1 + 1))) `2 ) by TOPREAL3:9
.= p `2 by A11, TOPREAL3:7
.= (((1 - r2) * (G * i2,j2)) `2 ) + ((r2 * (G * i2,(j2 + 1))) `2 ) by A14, TOPREAL3:7
.= ((1 - r2) * ((G * i2,j2) `2 )) + ((r2 * (G * i2,(j2 + 1))) `2 ) by TOPREAL3:9
.= ((1 - r2) * ((G * i1,j2) `2 )) + (r2 * ((G * i1,(j2 + 1)) `2 )) by A23, A24, TOPREAL3:9 ;

now

per cases ( j1 + 1 < j2 or j2 + 1 < j1 ) by A22, Th1;

suppose A26: j1 + 1 < j2 ; :: thesis: contradiction

j2 < j2 + 1 by XREAL_1:31;
then (G * i1,j2) `2 < (G * i1,(j2 + 1)) `2 by A1, A5, A6, GOBOARD5:5;
then ( ((1 - r2) * ((G * i1,j2) `2 )) + (r2 * ((G * i1,j2) `2 )) = 1 * ((G * i1,j2) `2 ) & r2 * ((G * i1,j2) `2 ) <= r2 * ((G * i1,(j2 + 1)) `2 ) ) by A15, XREAL_1:66;
then A27: (G * i1,j2) `2 <= ((1 - r2) * ((G * i1,j2) `2 )) + (r2 * ((G * i1,(j2 + 1)) `2 )) by XREAL_1:8;
j1 < j1 + 1 by XREAL_1:31;
then A28: (G * i1,j1) `2 <= (G * i1,(j1 + 1)) `2 by A1, A2, A3, GOBOARD5:5;
1 - r1 >= 0 by A13, XREAL_1:50;
then ( ((1 - r1) * ((G * i1,(j1 + 1)) `2 )) + (r1 * ((G * i1,(j1 + 1)) `2 )) = 1 * ((G * i1,(j1 + 1)) `2 ) & (1 - r1) * ((G * i1,j1) `2 ) <= (1 - r1) * ((G * i1,(j1 + 1)) `2 ) ) by A28, XREAL_1:66;
then A29: ((1 - r1) * ((G * i1,j1) `2 )) + (r1 * ((G * i1,(j1 + 1)) `2 )) <= (G * i1,(j1 + 1)) `2 by XREAL_1:8;
(G * i1,(j1 + 1)) `2 < (G * i1,j2) `2 by A1, A7, A18, A26, GOBOARD5:5;
hence contradiction by A25, A29, A27, XXREAL_0:2; :: thesis: verum

end;

suppose A30: j2 + 1 < j1 ; :: thesis: contradiction

j1 < j1 + 1 by XREAL_1:31;
then (G * i1,j1) `2 < (G * i1,(j1 + 1)) `2 by A1, A2, A3, GOBOARD5:5;
then ( ((1 - r1) * ((G * i1,j1) `2 )) + (r1 * ((G * i1,j1) `2 )) = 1 * ((G * i1,j1) `2 ) & r1 * ((G * i1,j1) `2 ) <= r1 * ((G * i1,(j1 + 1)) `2 ) ) by A12, XREAL_1:66;
then A31: (G * i1,j1) `2 <= ((1 - r1) * ((G * i1,j1) `2 )) + (r1 * ((G * i1,(j1 + 1)) `2 )) by XREAL_1:8;
j2 < j2 + 1 by XREAL_1:31;
then A32: (G * i1,j2) `2 <= (G * i1,(j2 + 1)) `2 by A1, A5, A6, GOBOARD5:5;
1 - r2 >= 0 by A16, XREAL_1:50;
then ( ((1 - r2) * ((G * i1,(j2 + 1)) `2 )) + (r2 * ((G * i1,(j2 + 1)) `2 )) = 1 * ((G * i1,(j2 + 1)) `2 ) & (1 - r2) * ((G * i1,j2) `2 ) <= (1 - r2) * ((G * i1,(j2 + 1)) `2 ) ) by A32, XREAL_1:66;
then A33: ((1 - r2) * ((G * i1,j2) `2 )) + (r2 * ((G * i1,(j2 + 1)) `2 )) <= (G * i1,(j2 + 1)) `2 by XREAL_1:8;
(G * i1,(j2 + 1)) `2 < (G * i1,j1) `2 by A1, A8, A17, A30, GOBOARD5:5;
hence contradiction by A25, A33, A31, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;