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,(GoB f) is convex & right_cell f,k,(GoB f) is convex )
let k be Element of NAT ; :: thesis: ( 1 <= k & k + 1 <= len f implies ( left_cell f,k,(GoB f) is convex & right_cell f,k,(GoB f) is convex ) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; :: thesis: ( left_cell f,k,(GoB f) is convex & right_cell f,k,(GoB f) is convex )
left_cell f,k = left_cell f,k,(GoB f) by A1, A2, JORDAN1H:27;
hence left_cell f,k,(GoB f) is convex by A1, A2, Th22; :: thesis: right_cell f,k,(GoB f) is convex
k <= len f by A2, NAT_1:13;
then A3: ((len f) -' k) + k = len f by XREAL_1:237;
then A4: (len f) -' k >= 1 by A2, XREAL_1:8;
then A5: right_cell f,k = left_cell (Rev f),((len f) -' k) by A1, A3, GOBOARD9:13;
( len f = len (Rev f) & ((len f) -' k) + 1 <= len f ) by A1, A3, FINSEQ_5:def 3, XREAL_1:8;
then left_cell (Rev f),((len f) -' k) is convex by A4, Th22;
hence right_cell f,k,(GoB f) is convex by A1, A2, A5, JORDAN1H:29; :: thesis: verum