let f be non constant standard special_circular_sequence; :: thesis: for k being Element of NAT st 1 <= k & k + 1 <= len f holds
left_cell f,k is convex
let k be Element of NAT ; :: thesis: ( 1 <= k & k + 1 <= len f implies left_cell f,k is convex )
assume A1: ( 1 <= k & k + 1 <= len f ) ; :: thesis: left_cell f,k is convex
consider i, j being Element of NAT such that
A2: ( i <= len (GoB f) & j <= width (GoB f) & cell (GoB f),i,j = left_cell f,k ) by A1, GOBOARD9:14;
thus left_cell f,k is convex by A2, Th21; :: thesis: verum