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,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds
i > 1

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 + 1)) & f /. (k + 1) = G * (i,j) holds
i > 1 )

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 + 1)) & f /. (k + 1) = G * (i,j) holds
i > 1

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 + 1)) & f /. (k + 1) = G * (i,j) implies i > 1 )
assume that
A2: ( 1 <= k & k + 1 <= len f ) and
A3: [i,j] in Indices G and
A4: ( [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) ) ; :: thesis: i > 1
assume A5: i <= 1 ; :: thesis: contradiction
1 <= i by ;
then i = 1 by ;
then A6: i -' 1 = 0 by XREAL_1:232;
A7: j <= width G by ;
right_cell (f,k,G) = cell (G,(i -' 1),j) by ;
then not (right_cell (f,k,G)) \ (L~ f) is bounded by ;
then not RightComp f is bounded by ;
then not BDD (L~ f) is bounded by GOBRD14:37;
hence contradiction by JORDAN2C:106; :: thesis: verum