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) )
A1: ( 1 <= 1 & 1 + 1 <= len f ) by GOBOARD7:36, XXREAL_0:2;
then 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,1 ) by GOBOARD9:14;
A3: Int (left_cell f,1) c= LeftComp f by A1, 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 A2, A3, XBOOLE_1:1; :: thesis: verum