let f be 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 Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds
(f /. k) `1 <> E-bound (L~ f)
let G be Go-board; :: thesis: ( 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) & f /. (k + 1) = G * (i,(j + 1)) holds
(f /. k) `1 <> E-bound (L~ f) )
assume A1: f is_sequence_on G ; :: thesis: 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) & f /. (k + 1) = G * (i,(j + 1)) holds
(f /. k) `1 <> E-bound (L~ f)
let i, j, k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) implies (f /. k) `1 <> E-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) and
A6: f /. (k + 1) = G * (i,(j + 1)) and
A7: (f /. k) `1 = E-bound (L~ f) ; :: thesis: contradiction
A8: right_cell (f,k,G) = cell (G,i,j) by A1, A2, A3, A4, A5, A6, GOBRD13:22;
A9: j <= width G by A3, MATRIX_0:32;
A10: ( 0 + 1 <= i & 1 <= j ) by A3, MATRIX_0:32;
set p = (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))));
A11: i <= len G by A3, MATRIX_0:32;
A12: j + 1 <= width G by A4, MATRIX_0:32;

per cases ( i = len G or i < len G ) by A11, XXREAL_0:1;

suppose i = len G ; :: thesis: contradiction

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

end;

suppose A13: i < len G ; :: thesis: contradiction

j < width G by A12, NAT_1:13;
then A14: Int (cell (G,i,j)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } by A10, A13, GOBOARD6:26;
i + 1 <= len G by A13, NAT_1:13;
then A15: (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) in Int (right_cell (f,k,G)) by A10, A12, A8, GOBOARD6:31;
then consider r, s being Real such that
A16: (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) = |[r,s]| and
A17: (G * (i,1)) `1 < r and
r < (G * ((i + 1),1)) `1 and
(G * (1,j)) `2 < s and
s < (G * (1,(j + 1))) `2 by A8, A14;
((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) `1 = r by A16, EUCLID:52;
then ((1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1))))) `1 > E-bound (L~ f) by A5, A7, A11, A10, A9, A17, GOBOARD5:2;
then A18: (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) in LeftComp f by Th10;
Int (right_cell (f,k,G)) c= RightComp f by A1, A2, JORDAN1H:25;
then (1 / 2) * ((G * (i,j)) + (G * ((i + 1),(j + 1)))) in (LeftComp f) /\ (RightComp f) by A15, A18, XBOOLE_0:def 4;
then LeftComp f meets RightComp f by XBOOLE_0:def 7;
hence contradiction by GOBRD14:14; :: thesis: verum

end;

end;