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

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

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

j > 1

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 j > 1 )

assume that

A2: ( 1 <= k & k + 1 <= len f ) and

A3: [i,j] in Indices G and

A4: ( [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) ) ; :: thesis: j > 1

assume A5: j <= 1 ; :: thesis: contradiction

1 <= j by A3, MATRIX_0:32;

then j = 1 by A5, XXREAL_0:1;

then A6: j -' 1 = 0 by XREAL_1:232;

A7: i <= len G by A3, MATRIX_0:32;

right_cell (f,k,G) = cell (G,i,(j -' 1)) by A1, A2, A3, A4, GOBRD13:24;

then not (right_cell (f,k,G)) \ (L~ f) is bounded by A7, A6, JORDAN1A:26, TOPREAL6:90;

then not RightComp f is bounded by A1, A2, JORDAN9:27, RLTOPSP1:42;

then not BDD (L~ f) is bounded by GOBRD14:37;

hence contradiction by JORDAN2C:106; :: thesis: verum

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

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

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

j > 1

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 j > 1 )

assume that

A2: ( 1 <= k & k + 1 <= len f ) and

A3: [i,j] in Indices G and

A4: ( [(i + 1),j] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * ((i + 1),j) ) ; :: thesis: j > 1

assume A5: j <= 1 ; :: thesis: contradiction

1 <= j by A3, MATRIX_0:32;

then j = 1 by A5, XXREAL_0:1;

then A6: j -' 1 = 0 by XREAL_1:232;

A7: i <= len G by A3, MATRIX_0:32;

right_cell (f,k,G) = cell (G,i,(j -' 1)) by A1, A2, A3, A4, GOBRD13:24;

then not (right_cell (f,k,G)) \ (L~ f) is bounded by A7, A6, JORDAN1A:26, TOPREAL6:90;

then not RightComp f is bounded by A1, A2, JORDAN9:27, RLTOPSP1:42;

then not BDD (L~ f) is bounded by GOBRD14:37;

hence contradiction by JORDAN2C:106; :: thesis: verum