let f be non constant standard special_circular_sequence; :: thesis: ex i, j being 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:34, XXREAL_0:2;
then A1: ( ex i, j being 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:11, GOBOARD9:21;
LeftComp f c= (LeftComp f) \/ (RightComp f) by XBOOLE_1:7;
hence ex i, j being 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