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

( ( i1 = i2 or i1 = i2 + 1 ) & ( j1 = j2 or j1 + 1 = j2 ) )

let i1, j1, i2, j2 be Nat; :: thesis: ( 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) implies ( ( i1 = i2 or i1 = i2 + 1 ) & ( j1 = j2 or j1 + 1 = j2 ) ) )

assume that

A1: 1 <= i1 and

A2: i1 <= len G and

A3: 1 <= j1 and

A4: j1 + 1 <= width G and

A5: 1 <= i2 and

A6: i2 + 1 <= len G and

A7: 1 <= j2 and

A8: j2 <= width G ; :: thesis: ( not LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) or ( ( i1 = i2 or i1 = i2 + 1 ) & ( j1 = j2 or j1 + 1 = j2 ) ) )

assume LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) ; :: thesis: ( ( i1 = i2 or i1 = i2 + 1 ) & ( j1 = j2 or j1 + 1 = j2 ) )

then consider x being object such that

A9: x in LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) 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,(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 + 1),j2))) and

A15: r2 >= 0 and

A16: r2 <= 1 by A10;

A17: i2 < len G by A6, NAT_1:13;

A18: 1 <= j1 + 1 by A3, NAT_1:13;

then A19: (G * (i1,(j1 + 1))) `2 = (G * (1,(j1 + 1))) `2 by A1, A2, A4, GOBOARD5:1

.= (G * (i2,(j1 + 1))) `2 by A4, A5, A18, A17, GOBOARD5:1 ;

A20: j1 < width G by A4, NAT_1:13;

then A21: (G * (i1,j1)) `2 = (G * (1,j1)) `2 by A1, A2, A3, GOBOARD5:1

.= (G * (i2,j1)) `2 by A3, A5, A20, A17, GOBOARD5:1 ;

A22: ((1 - r2) * ((G * (i2,j2)) `2)) + (r2 * ((G * ((i2 + 1),j2)) `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

.= p `2 by A14, TOPREAL3:2

.= (((1 - r1) * (G * (i1,j1))) `2) + ((r1 * (G * (i1,(j1 + 1)))) `2) by A11, TOPREAL3:2

.= ((1 - r1) * ((G * (i1,j1)) `2)) + ((r1 * (G * (i1,(j1 + 1)))) `2) by TOPREAL3:4

.= ((1 - r1) * ((G * (i2,j1)) `2)) + (r1 * ((G * (i2,(j1 + 1))) `2)) by A19, A21, TOPREAL3:4 ;

A23: 1 <= i2 + 1 by A5, NAT_1:13;

thus ( i1 = i2 or i1 = i2 + 1 ) :: thesis: ( j1 = j2 or j1 + 1 = j2 )

.= (G * ((i2 + 1),j2)) `2 by A6, A7, A8, A23, GOBOARD5:1 ;

assume A34: ( not j1 = j2 & not j1 + 1 = j2 ) ; :: thesis: contradiction

( ( i1 = i2 or i1 = i2 + 1 ) & ( j1 = j2 or j1 + 1 = j2 ) )

let i1, j1, i2, j2 be Nat; :: thesis: ( 1 <= i1 & i1 <= len G & 1 <= j1 & j1 + 1 <= width G & 1 <= i2 & i2 + 1 <= len G & 1 <= j2 & j2 <= width G & LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) implies ( ( i1 = i2 or i1 = i2 + 1 ) & ( j1 = j2 or j1 + 1 = j2 ) ) )

assume that

A1: 1 <= i1 and

A2: i1 <= len G and

A3: 1 <= j1 and

A4: j1 + 1 <= width G and

A5: 1 <= i2 and

A6: i2 + 1 <= len G and

A7: 1 <= j2 and

A8: j2 <= width G ; :: thesis: ( not LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) or ( ( i1 = i2 or i1 = i2 + 1 ) & ( j1 = j2 or j1 + 1 = j2 ) ) )

assume LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) meets LSeg ((G * (i2,j2)),(G * ((i2 + 1),j2))) ; :: thesis: ( ( i1 = i2 or i1 = i2 + 1 ) & ( j1 = j2 or j1 + 1 = j2 ) )

then consider x being object such that

A9: x in LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1)))) 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,(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 + 1),j2))) and

A15: r2 >= 0 and

A16: r2 <= 1 by A10;

A17: i2 < len G by A6, NAT_1:13;

A18: 1 <= j1 + 1 by A3, NAT_1:13;

then A19: (G * (i1,(j1 + 1))) `2 = (G * (1,(j1 + 1))) `2 by A1, A2, A4, GOBOARD5:1

.= (G * (i2,(j1 + 1))) `2 by A4, A5, A18, A17, GOBOARD5:1 ;

A20: j1 < width G by A4, NAT_1:13;

then A21: (G * (i1,j1)) `2 = (G * (1,j1)) `2 by A1, A2, A3, GOBOARD5:1

.= (G * (i2,j1)) `2 by A3, A5, A20, A17, GOBOARD5:1 ;

A22: ((1 - r2) * ((G * (i2,j2)) `2)) + (r2 * ((G * ((i2 + 1),j2)) `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

.= p `2 by A14, TOPREAL3:2

.= (((1 - r1) * (G * (i1,j1))) `2) + ((r1 * (G * (i1,(j1 + 1)))) `2) by A11, TOPREAL3:2

.= ((1 - r1) * ((G * (i1,j1)) `2)) + ((r1 * (G * (i1,(j1 + 1)))) `2) by TOPREAL3:4

.= ((1 - r1) * ((G * (i2,j1)) `2)) + (r1 * ((G * (i2,(j1 + 1))) `2)) by A19, A21, TOPREAL3:4 ;

A23: 1 <= i2 + 1 by A5, NAT_1:13;

thus ( i1 = i2 or i1 = i2 + 1 ) :: thesis: ( j1 = j2 or j1 + 1 = j2 )

proof

A33: (G * (i2,j2)) `2 =
(G * (1,j2)) `2
by A5, A7, A8, A17, GOBOARD5:1
A24: (G * (i2,j2)) `1 =
(G * (i2,1)) `1
by A5, A7, A8, A17, GOBOARD5:2

.= (G * (i2,j1)) `1 by A3, A5, A20, A17, GOBOARD5:2 ;

A25: (G * ((i2 + 1),j2)) `1 = (G * ((i2 + 1),1)) `1 by A6, A7, A8, A23, GOBOARD5:2

.= (G * ((i2 + 1),j1)) `1 by A3, A6, A20, A23, GOBOARD5:2 ;

A26: ((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:4

.= (((1 - r1) * (G * (i1,j1))) `1) + ((r1 * (G * (i1,(j1 + 1)))) `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 A25, A24, TOPREAL3:4 ;

A27: (G * (i1,j1)) `1 = (G * (i1,1)) `1 by A1, A2, A3, A20, GOBOARD5:2

.= (G * (i1,(j1 + 1))) `1 by A1, A2, A4, A18, GOBOARD5:2 ;

assume A28: ( not i1 = i2 & not i1 = i2 + 1 ) ; :: thesis: contradiction

end;.= (G * (i2,j1)) `1 by A3, A5, A20, A17, GOBOARD5:2 ;

A25: (G * ((i2 + 1),j2)) `1 = (G * ((i2 + 1),1)) `1 by A6, A7, A8, A23, GOBOARD5:2

.= (G * ((i2 + 1),j1)) `1 by A3, A6, A20, A23, GOBOARD5:2 ;

A26: ((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:4

.= (((1 - r1) * (G * (i1,j1))) `1) + ((r1 * (G * (i1,(j1 + 1)))) `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 A25, A24, TOPREAL3:4 ;

A27: (G * (i1,j1)) `1 = (G * (i1,1)) `1 by A1, A2, A3, A20, GOBOARD5:2

.= (G * (i1,(j1 + 1))) `1 by A1, A2, A4, A18, GOBOARD5:2 ;

assume A28: ( not i1 = i2 & not i1 = i2 + 1 ) ; :: thesis: contradiction

per cases
( ( i1 < i2 & i1 < i2 + 1 ) or ( i1 < i2 & i2 + 1 < i1 ) or ( i2 < i1 & i1 < i2 + 1 ) or i2 + 1 < i1 )
by A28, XXREAL_0:1;

end;

suppose A29:
( i1 < i2 & i1 < i2 + 1 )
; :: thesis: contradiction

i2 < i2 + 1
by XREAL_1:29;

then (G * (i2,j1)) `1 < (G * ((i2 + 1),j1)) `1 by A3, A5, A6, A20, GOBOARD5:3;

then A30: ( ((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;

(G * (i1,j1)) `1 < (G * (i2,j1)) `1 by A1, A3, A20, A17, A29, GOBOARD5:3;

hence contradiction by A26, A27, A30, XREAL_1:6; :: thesis: verum

end;then (G * (i2,j1)) `1 < (G * ((i2 + 1),j1)) `1 by A3, A5, A6, A20, GOBOARD5:3;

then A30: ( ((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;

(G * (i1,j1)) `1 < (G * (i2,j1)) `1 by A1, A3, A20, A17, A29, GOBOARD5:3;

hence contradiction by A26, A27, A30, XREAL_1:6; :: thesis: verum

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

i2 < i2 + 1
by XREAL_1:29;

then A32: (G * (i2,j1)) `1 <= (G * ((i2 + 1),j1)) `1 by A3, A5, A6, A20, 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 ((1 - r2) * ((G * (i2,j1)) `1)) + (r2 * ((G * ((i2 + 1),j1)) `1)) <= (G * ((i2 + 1),j1)) `1 by XREAL_1:6;

hence contradiction by A2, A3, A20, A23, A26, A27, A31, GOBOARD5:3; :: thesis: verum

end;then A32: (G * (i2,j1)) `1 <= (G * ((i2 + 1),j1)) `1 by A3, A5, A6, A20, 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 ((1 - r2) * ((G * (i2,j1)) `1)) + (r2 * ((G * ((i2 + 1),j1)) `1)) <= (G * ((i2 + 1),j1)) `1 by XREAL_1:6;

hence contradiction by A2, A3, A20, A23, A26, A27, A31, GOBOARD5:3; :: thesis: verum

.= (G * ((i2 + 1),j2)) `2 by A6, A7, A8, A23, GOBOARD5:1 ;

assume A34: ( not j1 = j2 & not j1 + 1 = j2 ) ; :: thesis: contradiction

per cases
( ( j2 < j1 & j2 < j1 + 1 ) or ( j2 < j1 & j1 + 1 < j2 ) or ( j1 < j2 & j2 < j1 + 1 ) or j1 + 1 < j2 )
by A34, XXREAL_0:1;

end;

suppose A35:
( j2 < j1 & j2 < j1 + 1 )
; :: thesis: contradiction

j1 < j1 + 1
by XREAL_1:29;

then (G * (i2,j1)) `2 < (G * (i2,(j1 + 1))) `2 by A3, A4, A5, A17, GOBOARD5:4;

then A36: ( ((1 - r1) * ((G * (i2,j1)) `2)) + (r1 * ((G * (i2,j1)) `2)) = 1 * ((G * (i2,j1)) `2) & r1 * ((G * (i2,j1)) `2) <= r1 * ((G * (i2,(j1 + 1))) `2) ) by A12, XREAL_1:64;

(G * (i2,j2)) `2 < (G * (i2,j1)) `2 by A5, A7, A20, A17, A35, GOBOARD5:4;

hence contradiction by A22, A33, A36, XREAL_1:6; :: thesis: verum

end;then (G * (i2,j1)) `2 < (G * (i2,(j1 + 1))) `2 by A3, A4, A5, A17, GOBOARD5:4;

then A36: ( ((1 - r1) * ((G * (i2,j1)) `2)) + (r1 * ((G * (i2,j1)) `2)) = 1 * ((G * (i2,j1)) `2) & r1 * ((G * (i2,j1)) `2) <= r1 * ((G * (i2,(j1 + 1))) `2) ) by A12, XREAL_1:64;

(G * (i2,j2)) `2 < (G * (i2,j1)) `2 by A5, A7, A20, A17, A35, GOBOARD5:4;

hence contradiction by A22, A33, A36, XREAL_1:6; :: thesis: verum

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

j1 < j1 + 1
by XREAL_1:29;

then A38: (G * (i2,j1)) `2 <= (G * (i2,(j1 + 1))) `2 by A3, A4, A5, A17, GOBOARD5:4;

1 - r1 >= 0 by A13, XREAL_1:48;

then ( ((1 - r1) * ((G * (i2,(j1 + 1))) `2)) + (r1 * ((G * (i2,(j1 + 1))) `2)) = 1 * ((G * (i2,(j1 + 1))) `2) & (1 - r1) * ((G * (i2,j1)) `2) <= (1 - r1) * ((G * (i2,(j1 + 1))) `2) ) by A38, XREAL_1:64;

then ((1 - r1) * ((G * (i2,j1)) `2)) + (r1 * ((G * (i2,(j1 + 1))) `2)) <= (G * (i2,(j1 + 1))) `2 by XREAL_1:6;

hence contradiction by A5, A8, A18, A17, A22, A33, A37, GOBOARD5:4; :: thesis: verum

end;then A38: (G * (i2,j1)) `2 <= (G * (i2,(j1 + 1))) `2 by A3, A4, A5, A17, GOBOARD5:4;

1 - r1 >= 0 by A13, XREAL_1:48;

then ( ((1 - r1) * ((G * (i2,(j1 + 1))) `2)) + (r1 * ((G * (i2,(j1 + 1))) `2)) = 1 * ((G * (i2,(j1 + 1))) `2) & (1 - r1) * ((G * (i2,j1)) `2) <= (1 - r1) * ((G * (i2,(j1 + 1))) `2) ) by A38, XREAL_1:64;

then ((1 - r1) * ((G * (i2,j1)) `2)) + (r1 * ((G * (i2,(j1 + 1))) `2)) <= (G * (i2,(j1 + 1))) `2 by XREAL_1:6;

hence contradiction by A5, A8, A18, A17, A22, A33, A37, GOBOARD5:4; :: thesis: verum