let f be non constant standard special_circular_sequence; :: thesis: ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & Int (cell (GoB f),i,j) c= (LeftComp f) \/ (RightComp f) )
1 + 1 <= len f by GOBOARD7:36, XXREAL_0:2;
then A1: ( ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & cell (GoB f),i,j = left_cell f,1 ) & Int (left_cell f,1) c= LeftComp f ) by GOBOARD9:14, GOBOARD9:24;
LeftComp f c= (LeftComp f) \/ (RightComp f) by XBOOLE_1:7;
hence ex i, j being Element of NAT st
( i <= len (GoB f) & j <= width (GoB f) & Int (cell (GoB f),i,j) c= (LeftComp f) \/ (RightComp f) ) by A1, XBOOLE_1:1; :: thesis: verum