let f be non constant standard special_circular_sequence; :: thesis: for k being Nat st 1 <= k & k + 1 <= len f holds

left_cell (f,k) is convex

let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f implies left_cell (f,k) is convex )

assume ( 1 <= k & k + 1 <= len f ) ; :: thesis: left_cell (f,k) is convex

then ex i, j being Nat st

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) by GOBOARD9:11;

hence left_cell (f,k) is convex by Th20; :: thesis: verum

left_cell (f,k) is convex

let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f implies left_cell (f,k) is convex )

assume ( 1 <= k & k + 1 <= len f ) ; :: thesis: left_cell (f,k) is convex

then ex i, j being Nat st

( i <= len (GoB f) & j <= width (GoB f) & cell ((GoB f),i,j) = left_cell (f,k) ) by GOBOARD9:11;

hence left_cell (f,k) is convex by Th20; :: thesis: verum