let f be V22() 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 + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds
(f /. k) `2 <> S-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 + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds
(f /. k) `2 <> S-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 + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) holds
(f /. k) `2 <> S-bound (L~ f)

let i, j, k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) implies (f /. k) `2 <> S-bound (L~ f) )
assume that
A2: ( 1 <= k & k + 1 <= len f ) and
A3: [i,j] in Indices G and
A4: [(i + 1),j] in Indices G and
A5: f /. k = G * (i,j) and
A6: f /. (k + 1) = G * ((i + 1),j) and
A7: (f /. k) `2 = S-bound (L~ f) ; :: thesis: contradiction
A8: right_cell (f,k,G) = cell (G,i,(j -' 1)) by A1, A2, A3, A4, A5, A6, GOBRD13:24;
A9: i <= len G by ;
A10: j <= width G by ;
A11: i + 1 <= len G by ;
set p = (1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j)));
A12: 0 + 1 <= i by ;
A13: 1 <= j by ;
then A14: (j -' 1) + 1 = j by XREAL_1:235;
per cases ( j = 1 or j > 1 ) by ;
suppose j = 1 ; :: thesis: contradiction
end;
suppose j > 1 ; :: thesis: contradiction
then j >= 1 + 1 by NAT_1:13;
then A15: j - 1 >= (1 + 1) - 1 by XREAL_1:9;
j < () + 1 by ;
then A16: j - 1 < (() + 1) - 1 by XREAL_1:9;
i < len G by ;
then A17: Int (cell (G,i,(j -' 1))) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 & (G * (1,(j -' 1))) `2 < s & s < (G * (1,j)) `2 ) } by ;
A18: (1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j))) in Int (right_cell (f,k,G)) by ;
then consider r, s being Real such that
A19: (1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j))) = |[r,s]| and
(G * (i,1)) `1 < r and
r < (G * ((i + 1),1)) `1 and
(G * (1,(j -' 1))) `2 < s and
A20: s < (G * (1,j)) `2 by ;
((1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j)))) `2 = s by ;
then ((1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j)))) `2 < S-bound (L~ f) by A5, A7, A12, A9, A13, A10, A20, GOBOARD5:1;
then A21: (1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j))) in LeftComp f by Th11;
Int (right_cell (f,k,G)) c= RightComp f by ;
then (1 / 2) * ((G * (i,(j -' 1))) + (G * ((i + 1),j))) in () /\ () by ;
then LeftComp f meets RightComp f by XBOOLE_0:def 7;
hence contradiction by GOBRD14:14; :: thesis: verum
end;
end;