let f be V22() standard clockwise_oriented special_circular_sequence; for G being Go-board st f is_sequence_on G holds
for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds
(f /. k) `1 <> W-bound (L~ f)
let G be Go-board; ( f is_sequence_on G implies for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds
(f /. k) `1 <> W-bound (L~ f) )
assume A1:
f is_sequence_on G
; for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds
(f /. k) `1 <> W-bound (L~ f)
let i, j, k be Nat; ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) implies (f /. k) `1 <> W-bound (L~ f) )
assume that
A2:
( 1 <= k & k + 1 <= len f )
and
A3:
[i,j] in Indices G
and
A4:
[i,(j + 1)] in Indices G
and
A5:
f /. k = G * (i,(j + 1))
and
A6:
f /. (k + 1) = G * (i,j)
and
A7:
(f /. k) `1 = W-bound (L~ f)
; contradiction
A8:
right_cell (f,k,G) = cell (G,(i -' 1),j)
by A1, A2, A3, A4, A5, A6, GOBRD13:28;
A9:
( 1 <= i & i <= len G )
by A4, MATRIX_0:32;
A10:
1 <= j
by A3, MATRIX_0:32;
A11:
1 <= j + 1
by A4, MATRIX_0:32;
A12:
j + 1 <= width G
by A4, MATRIX_0:32;
set p = (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1))));
A13:
i <= len G
by A3, MATRIX_0:32;
A14:
0 + 1 <= i
by A3, MATRIX_0:32;
then A15:
(i -' 1) + 1 = i
by XREAL_1:235;
per cases
( i = 1 or i > 1 )
by A14, XXREAL_0:1;
suppose
i > 1
;
contradictionthen
i >= 1
+ 1
by NAT_1:13;
then A16:
i - 1
>= (1 + 1) - 1
by XREAL_1:9;
i < (len G) + 1
by A13, NAT_1:13;
then A17:
i - 1
< ((len G) + 1) - 1
by XREAL_1:9;
j < width G
by A12, NAT_1:13;
then A18:
Int (cell (G,(i -' 1),j)) = { |[r,s]| where r, s is Real : ( (G * ((i -' 1),1)) `1 < r & r < (G * (i,1)) `1 & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) }
by A10, A15, A16, A17, GOBOARD6:26;
A19:
(1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) in Int (right_cell (f,k,G))
by A13, A10, A12, A8, A15, A16, GOBOARD6:31;
then consider r,
s being
Real such that A20:
(1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) = |[r,s]|
and
(G * ((i -' 1),1)) `1 < r
and A21:
r < (G * (i,1)) `1
and
(G * (1,j)) `2 < s
and
s < (G * (1,(j + 1))) `2
by A8, A18;
((1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1))))) `1 = r
by A20, EUCLID:52;
then
((1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1))))) `1 < W-bound (L~ f)
by A5, A7, A9, A11, A12, A21, GOBOARD5:2;
then A22:
(1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) in LeftComp f
by Th9;
Int (right_cell (f,k,G)) c= RightComp f
by A1, A2, JORDAN1H:25;
then
(1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) in (LeftComp f) /\ (RightComp f)
by A19, A22, XBOOLE_0:def 4;
then
LeftComp f meets RightComp f
by XBOOLE_0:def 7;
hence
contradiction
by GOBRD14:14;
verum end; end;