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 + 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 Element of 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 Element of 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
A2: L~ f is Bounded by JORDAN2C:73;
let i, j, k be Element of 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
A3: ( 1 <= k & k + 1 <= len f ) and
A4: [i,j] in Indices G and
A5: ( [(i + 1),j] in Indices G & f /. k = G * i,j & f /. (k + 1) = G * (i + 1),j ) ; :: thesis: j > 1
assume A6: j <= 1 ; :: thesis: contradiction
1 <= j by A4, MATRIX_1:39;
then j = 1 by A6, XXREAL_0:1;
then A7: j -' 1 = 0 by XREAL_1:234;
A8: i <= len G by A4, MATRIX_1:39;
right_cell f,k,G = cell G,i,(j -' 1) by A1, A3, A4, A5, GOBRD13:25;
then not (right_cell f,k,G) \ (L~ f) is Bounded by A8, A7, A2, JORDAN1A:47, TOPREAL6:99;
then not RightComp f is Bounded by A1, A3, JORDAN2C:16, JORDAN9:29;
then not BDD (L~ f) is Bounded by GOBRD14:47;
hence contradiction by JORDAN2C:73, JORDAN2C:114; :: thesis: verum