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

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

suppose j1 <> j2 ; :: thesis: contradiction

then A14: ( j1 < j2 or j2 < j1 ) by XXREAL_0:1;
A15: (G * i1,j1) `2 = (G * 1,j1) `2 by A1, A2, A12, GOBOARD5:2
.= (G * (i1 + 1),j1) `2 by A1, A2, A12, GOBOARD5:2 ;
A16: (G * i2,j2) `2 = (G * 1,j2) `2 by A3, A4, A13, GOBOARD5:2
.= (G * (i2 + 1),j2) `2 by A3, A4, A13, GOBOARD5:2 ;
1 * ((G * i1,j1) `2 ) = ((1 - r1) * ((G * i1,j1) `2 )) + (r1 * ((G * (i1 + 1),j1) `2 )) by A15
.= (((1 - r1) * (G * i1,j1)) `2 ) + (r1 * ((G * (i1 + 1),j1) `2 )) by TOPREAL3:9
.= (((1 - r1) * (G * i1,j1)) `2 ) + ((r1 * (G * (i1 + 1),j1)) `2 ) by TOPREAL3:9
.= p `2 by A8, TOPREAL3:7
.= (((1 - r2) * (G * i2,j2)) `2 ) + ((r2 * (G * (i2 + 1),j2)) `2 ) by A10, TOPREAL3:7
.= ((1 - r2) * ((G * i2,j2) `2 )) + ((r2 * (G * (i2 + 1),j2)) `2 ) by TOPREAL3:9
.= ((1 - r2) * ((G * i2,j2) `2 )) + (r2 * ((G * (i2 + 1),j2) `2 )) by TOPREAL3:9
.= (G * 1,j2) `2 by A3, A4, A13, A16, GOBOARD5:2
.= (G * i1,j2) `2 by A1, A4, A12, GOBOARD5:2 ;
hence contradiction by A1, A2, A4, A12, A14, GOBOARD5:5; :: thesis: verum

end;

suppose A17: abs (i1 - i2) > 1 ; :: thesis: contradiction

A18: (G * (i2 + 1),j2) `1 = (G * (i2 + 1),1) `1 by A3, A4, A13, GOBOARD5:3
.= (G * (i2 + 1),j1) `1 by A2, A3, A13, GOBOARD5:3 ;
A19: (G * i2,j2) `1 = (G * i2,1) `1 by A3, A4, A13, GOBOARD5:3
.= (G * i2,j1) `1 by A2, A3, A13, GOBOARD5:3 ;
A20: ((1 - r1) * ((G * i1,j1) `1 )) + (r1 * ((G * (i1 + 1),j1) `1 )) = (((1 - r1) * (G * i1,j1)) `1 ) + (r1 * ((G * (i1 + 1),j1) `1 )) by TOPREAL3:9
.= (((1 - r1) * (G * i1,j1)) `1 ) + ((r1 * (G * (i1 + 1),j1)) `1 ) by TOPREAL3:9
.= p `1 by A8, TOPREAL3:7
.= (((1 - r2) * (G * i2,j2)) `1 ) + ((r2 * (G * (i2 + 1),j2)) `1 ) by A10, TOPREAL3:7
.= ((1 - r2) * ((G * i2,j2) `1 )) + ((r2 * (G * (i2 + 1),j2)) `1 ) by TOPREAL3:9
.= ((1 - r2) * ((G * i2,j1) `1 )) + (r2 * ((G * (i2 + 1),j1) `1 )) by A18, A19, TOPREAL3:9 ;

now

per cases ( i1 + 1 < i2 or i2 + 1 < i1 ) by A17, Th1;

suppose i1 + 1 < i2 ; :: thesis: contradiction

then A21: (G * (i1 + 1),j1) `1 < (G * i2,j1) `1 by A2, A12, A13, GOBOARD5:4;
A22: ((1 - r1) * ((G * (i1 + 1),j1) `1 )) + (r1 * ((G * (i1 + 1),j1) `1 )) = 1 * ((G * (i1 + 1),j1) `1 ) ;
A23: ((1 - r2) * ((G * i2,j1) `1 )) + (r2 * ((G * i2,j1) `1 )) = 1 * ((G * i2,j1) `1 ) ;
A24: 1 - r1 >= 0 by A7, XREAL_1:50;
i1 < i1 + 1 by XREAL_1:31;
then (G * i1,j1) `1 <= (G * (i1 + 1),j1) `1 by A1, A2, GOBOARD5:4;
then (1 - r1) * ((G * i1,j1) `1 ) <= (1 - r1) * ((G * (i1 + 1),j1) `1 ) by A24, XREAL_1:66;
then A25: ((1 - r1) * ((G * i1,j1) `1 )) + (r1 * ((G * (i1 + 1),j1) `1 )) <= (G * (i1 + 1),j1) `1 by A22, XREAL_1:8;
i2 < i2 + 1 by XREAL_1:31;
then (G * i2,j1) `1 < (G * (i2 + 1),j1) `1 by A2, A3, GOBOARD5:4;
then r2 * ((G * i2,j1) `1 ) <= r2 * ((G * (i2 + 1),j1) `1 ) by A9, XREAL_1:66;
then (G * i2,j1) `1 <= ((1 - r2) * ((G * i2,j1) `1 )) + (r2 * ((G * (i2 + 1),j1) `1 )) by A23, XREAL_1:8;
hence contradiction by A20, A21, A25, XXREAL_0:2; :: thesis: verum

end;

suppose i2 + 1 < i1 ; :: thesis: contradiction

then A26: (G * (i2 + 1),j1) `1 < (G * i1,j1) `1 by A2, A12, A13, GOBOARD5:4;
A27: ((1 - r1) * ((G * i1,j1) `1 )) + (r1 * ((G * i1,j1) `1 )) = 1 * ((G * i1,j1) `1 ) ;
A28: ((1 - r2) * ((G * (i2 + 1),j1) `1 )) + (r2 * ((G * (i2 + 1),j1) `1 )) = 1 * ((G * (i2 + 1),j1) `1 ) ;
A29: 1 - r2 >= 0 by A9, XREAL_1:50;
i2 < i2 + 1 by XREAL_1:31;
then (G * i2,j1) `1 <= (G * (i2 + 1),j1) `1 by A2, A3, GOBOARD5:4;
then (1 - r2) * ((G * i2,j1) `1 ) <= (1 - r2) * ((G * (i2 + 1),j1) `1 ) by A29, XREAL_1:66;
then A30: ((1 - r2) * ((G * i2,j1) `1 )) + (r2 * ((G * (i2 + 1),j1) `1 )) <= (G * (i2 + 1),j1) `1 by A28, XREAL_1:8;
i1 < i1 + 1 by XREAL_1:31;
then (G * i1,j1) `1 < (G * (i1 + 1),j1) `1 by A1, A2, GOBOARD5:4;
then r1 * ((G * i1,j1) `1 ) <= r1 * ((G * (i1 + 1),j1) `1 ) by A7, XREAL_1:66;
then (G * i1,j1) `1 <= ((1 - r1) * ((G * i1,j1) `1 )) + (r1 * ((G * (i1 + 1),j1) `1 )) by A27, XREAL_1:8;
hence contradiction by A20, A26, A30, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;