let G be Go-board; 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; ( 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
; ( 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)))
; ( ( 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 )
( j1 = j2 or j1 + 1 = j2 )proof
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 )
;
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;
suppose A29:
(
i1 < i2 &
i1 < i2 + 1 )
;
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;
verum end; suppose
(
i1 < i2 &
i2 + 1
< i1 )
;
contradictionend; suppose
(
i2 < i1 &
i1 < i2 + 1 )
;
contradictionend; suppose A31:
i2 + 1
< i1
;
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;
verum end;
end;
A33: (G * (i2,j2)) `2 =
(G * (1,j2)) `2
by A5, A7, A8, A17, GOBOARD5:1
.=
(G * ((i2 + 1),j2)) `2
by A6, A7, A8, A23, GOBOARD5:1
;
assume A34:
( not j1 = j2 & not j1 + 1 = j2 )
; 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;
suppose A35:
(
j2 < j1 &
j2 < j1 + 1 )
;
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;
verum end; suppose
(
j2 < j1 &
j1 + 1
< j2 )
;
contradictionend; suppose
(
j1 < j2 &
j2 < j1 + 1 )
;
contradictionend; suppose A37:
j1 + 1
< j2
;
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;
verum end;