let G be Go-board; :: thesis: for i1, j1, i2, j2 being 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 & |.(i1 - i2).| <= 1 )
let i1, j1, i2, j2 be 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 & |.(i1 - i2).| <= 1 ) )
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 LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) or ( j1 = j2 & |.(i1 - i2).| <= 1 ) )
A7: 1 <= i1 + 1 by A1, NAT_1:13;
A8: i1 < len G by A2, NAT_1:13;
assume LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) ; :: thesis: ( j1 = j2 & |.(i1 - i2).| <= 1 )
then consider x being object such that
A9: x in LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1))) and
A10: x in LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) 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 + 1),j1))) 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 + 1),j2))) and
A15: r2 >= 0 and
A16: r2 <= 1 by A10;
A17: 1 <= i2 + 1 by A4, NAT_1:13;
A18: i2 < len G by A5, NAT_1:13;
assume A19: ( not j1 = j2 or not |.(i1 - i2).| <= 1 ) ; :: thesis: contradiction

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

suppose j1 <> j2 ; :: thesis: contradiction

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

end;

suppose A22: |.(i1 - i2).| > 1 ; :: thesis: contradiction

A23: (G * ((i2 + 1),j2)) `1 = (G * ((i2 + 1),1)) `1 by A5, A6, A17, GOBOARD5:2
.= (G * ((i2 + 1),j1)) `1 by A3, A5, A17, GOBOARD5:2 ;
A24: (G * (i2,j2)) `1 = (G * (i2,1)) `1 by A4, A6, A18, GOBOARD5:2
.= (G * (i2,j1)) `1 by A3, A4, A18, GOBOARD5:2 ;
A25: ((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:4
.= (((1 - r1) * (G * (i1,j1))) `1) + ((r1 * (G * ((i1 + 1),j1))) `1) by TOPREAL3:4
.= p `1 by A11, TOPREAL3:2
.= (((1 - r2) * (G * (i2,j2))) `1) + ((r2 * (G * ((i2 + 1),j2))) `1) by A14, TOPREAL3:2
.= ((1 - r2) * ((G * (i2,j2)) `1)) + ((r2 * (G * ((i2 + 1),j2))) `1) by TOPREAL3:4
.= ((1 - r2) * ((G * (i2,j1)) `1)) + (r2 * ((G * ((i2 + 1),j1)) `1)) by A23, A24, TOPREAL3:4 ;

now :: thesis: contradiction

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

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

i2 < i2 + 1 by XREAL_1:29;
then (G * (i2,j1)) `1 < (G * ((i2 + 1),j1)) `1 by A3, A4, A5, GOBOARD5:3;
then ( ((1 - r2) * ((G * (i2,j1)) `1)) + (r2 * ((G * (i2,j1)) `1)) = 1 * ((G * (i2,j1)) `1) & r2 * ((G * (i2,j1)) `1) <= r2 * ((G * ((i2 + 1),j1)) `1) ) by A15, XREAL_1:64;
then A27: (G * (i2,j1)) `1 <= ((1 - r2) * ((G * (i2,j1)) `1)) + (r2 * ((G * ((i2 + 1),j1)) `1)) by XREAL_1:6;
i1 < i1 + 1 by XREAL_1:29;
then A28: (G * (i1,j1)) `1 <= (G * ((i1 + 1),j1)) `1 by A1, A2, A3, GOBOARD5:3;
1 - r1 >= 0 by A13, XREAL_1:48;
then ( ((1 - r1) * ((G * ((i1 + 1),j1)) `1)) + (r1 * ((G * ((i1 + 1),j1)) `1)) = 1 * ((G * ((i1 + 1),j1)) `1) & (1 - r1) * ((G * (i1,j1)) `1) <= (1 - r1) * ((G * ((i1 + 1),j1)) `1) ) by A28, XREAL_1:64;
then A29: ((1 - r1) * ((G * (i1,j1)) `1)) + (r1 * ((G * ((i1 + 1),j1)) `1)) <= (G * ((i1 + 1),j1)) `1 by XREAL_1:6;
(G * ((i1 + 1),j1)) `1 < (G * (i2,j1)) `1 by A3, A7, A18, A26, GOBOARD5:3;
hence contradiction by A25, A29, A27, XXREAL_0:2; :: thesis: verum

end;

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

i1 < i1 + 1 by XREAL_1:29;
then (G * (i1,j1)) `1 < (G * ((i1 + 1),j1)) `1 by A1, A2, A3, GOBOARD5:3;
then ( ((1 - r1) * ((G * (i1,j1)) `1)) + (r1 * ((G * (i1,j1)) `1)) = 1 * ((G * (i1,j1)) `1) & r1 * ((G * (i1,j1)) `1) <= r1 * ((G * ((i1 + 1),j1)) `1) ) by A12, XREAL_1:64;
then A31: (G * (i1,j1)) `1 <= ((1 - r1) * ((G * (i1,j1)) `1)) + (r1 * ((G * ((i1 + 1),j1)) `1)) by XREAL_1:6;
i2 < i2 + 1 by XREAL_1:29;
then A32: (G * (i2,j1)) `1 <= (G * ((i2 + 1),j1)) `1 by A3, A4, A5, GOBOARD5:3;
1 - r2 >= 0 by A16, XREAL_1:48;
then ( ((1 - r2) * ((G * ((i2 + 1),j1)) `1)) + (r2 * ((G * ((i2 + 1),j1)) `1)) = 1 * ((G * ((i2 + 1),j1)) `1) & (1 - r2) * ((G * (i2,j1)) `1) <= (1 - r2) * ((G * ((i2 + 1),j1)) `1) ) by A32, XREAL_1:64;
then A33: ((1 - r2) * ((G * (i2,j1)) `1)) + (r2 * ((G * ((i2 + 1),j1)) `1)) <= (G * ((i2 + 1),j1)) `1 by XREAL_1:6;
(G * ((i2 + 1),j1)) `1 < (G * (i1,j1)) `1 by A3, A8, A17, A30, GOBOARD5:3;
hence contradiction by A25, A33, A31, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;