let f be non constant standard clockwise_oriented special_circular_sequence; :: thesis: for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of 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; :: thesis: ( f is_sequence_on G implies for i, j, k being Element of 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 ; :: thesis: for i, j, k being Element of 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 Element of NAT ; :: thesis: ( 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) ; :: thesis: contradiction
A8: ( 0 + 1 <= i & i <= len G & 1 <= j & j <= width G ) by A3, MATRIX_1:39;
A9: ( 1 <= i & i <= len G & 1 <= j + 1 & j + 1 <= width G ) by A4, MATRIX_1:39;
A10: right_cell f,k,G = cell G,(i -' 1),j by A1, A2, A3, A4, A5, A6, GOBRD13:29;
set p = (1 / 2) * ((G * (i -' 1),j) + (G * i,(j + 1)));
A11: (i -' 1) + 1 = i by A8, XREAL_1:237;

per cases ( i = 1 or i > 1 ) by A8, XXREAL_0:1;

suppose i = 1 ; :: thesis: contradiction

hence contradiction by A1, A2, A3, A4, A5, A6, Th18; :: thesis: verum

end;

suppose i > 1 ; :: thesis: contradiction

then i >= 1 + 1 by NAT_1:13;
then A12: i - 1 >= (1 + 1) - 1 by XREAL_1:11;
then A13: (1 / 2) * ((G * (i -' 1),j) + (G * i,(j + 1))) in Int (right_cell f,k,G) by A8, A9, A10, A11, GOBOARD6:34;
i < (len G) + 1 by A8, NAT_1:13;
then A14: i - 1 < ((len G) + 1) - 1 by XREAL_1:11;
j < width G by A9, NAT_1:13;
then 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 A8, A11, A12, A14, GOBOARD6:29;
then consider r, s being Real such that
A15: (1 / 2) * ((G * (i -' 1),j) + (G * i,(j + 1))) = |[r,s]| and
(G * (i -' 1),1) `1 < r and
A16: r < (G * i,1) `1 and
(G * 1,j) `2 < s and
s < (G * 1,(j + 1)) `2 by A10, A13;
((1 / 2) * ((G * (i -' 1),j) + (G * i,(j + 1)))) `1 = r by A15, EUCLID:56;
then ((1 / 2) * ((G * (i -' 1),j) + (G * i,(j + 1)))) `1 < W-bound (L~ f) by A5, A7, A9, A16, GOBOARD5:3;
then A17: (1 / 2) * ((G * (i -' 1),j) + (G * i,(j + 1))) in LeftComp f by Th11;
Int (right_cell f,k,G) c= RightComp f by A1, A2, JORDAN1H:31;
then (1 / 2) * ((G * (i -' 1),j) + (G * i,(j + 1))) in (LeftComp f) /\ (RightComp f) by A13, A17, XBOOLE_0:def 4;
then LeftComp f meets RightComp f by XBOOLE_0:def 7;
hence contradiction by GOBRD14:24; :: thesis: verum

end;

end;