let i be Nat; :: thesis: for G being Go-board st i <= len G holds
not cell (G,i,0) is bounded
let G be Go-board; :: thesis: ( i <= len G implies not cell (G,i,0) is bounded )
assume A1: i <= len G ; :: thesis: not cell (G,i,0) is bounded

per cases ( i = 0 or ( i >= 1 & i < len G ) or i = len G ) by A1, NAT_1:14, XXREAL_0:1;

suppose i = 0 ; :: thesis: not cell (G,i,0) is bounded

then A2: cell (G,i,0) = { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & s <= (G * (1,1)) `2 ) } by GOBRD11:24;
for r being Real ex q being Point of (TOP-REAL 2) st
( q in cell (G,i,0) & not |.q.| < r )

proof

let r be Real; :: thesis: ex q being Point of (TOP-REAL 2) st
( q in cell (G,i,0) & not |.q.| < r )
take q = |[(min ((- r),((G * (1,1)) `1))),(min ((- r),((G * (1,1)) `2)))]|; :: thesis: ( q in cell (G,i,0) & not |.q.| < r )
A3: |.(q `1).| <= |.q.| by JGRAPH_1:33;
( min ((- r),((G * (1,1)) `1)) <= (G * (1,1)) `1 & min ((- r),((G * (1,1)) `2)) <= (G * (1,1)) `2 ) by XXREAL_0:17;
hence q in cell (G,i,0) by A2; :: thesis: not |.q.| < r

per cases ( r <= 0 or r > 0 ) ;

suppose r <= 0 ; :: thesis: not |.q.| < r

hence not |.q.| < r ; :: thesis: verum

end;

suppose A4: r > 0 ; :: thesis: not |.q.| < r

q `1 = min ((- r),((G * (1,1)) `1)) by EUCLID:52;
then A5: |.(- r).| <= |.(q `1).| by A4, TOPREAL6:3, XXREAL_0:17;
- (- r) > 0 by A4;
then - r < 0 ;
then - (- r) <= |.(q `1).| by A5, ABSVALUE:def 1;
hence not |.q.| < r by A3, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence not cell (G,i,0) is bounded by JORDAN2C:34; :: thesis: verum

end;

suppose A6: ( i >= 1 & i < len G ) ; :: thesis: not cell (G,i,0) is bounded

then A7: cell (G,i,0) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & s <= (G * (1,1)) `2 ) } by GOBRD11:30;
for r being Real ex q being Point of (TOP-REAL 2) st
( q in cell (G,i,0) & not |.q.| < r )

proof

let r be Real; :: thesis: ex q being Point of (TOP-REAL 2) st
( q in cell (G,i,0) & not |.q.| < r )
take q = |[((G * (i,1)) `1),(min ((- r),((G * (1,1)) `2)))]|; :: thesis: ( q in cell (G,i,0) & not |.q.| < r )
A8: min ((- r),((G * (1,1)) `2)) <= (G * (1,1)) `2 by XXREAL_0:17;
width G <> 0 by MATRIX_0:def 10;
then A9: 1 <= width G by NAT_1:14;
( i < i + 1 & i + 1 <= len G ) by A6, NAT_1:13;
then (G * (i,1)) `1 <= (G * ((i + 1),1)) `1 by A6, A9, GOBOARD5:3;
hence q in cell (G,i,0) by A7, A8; :: thesis: not |.q.| < r
A10: |.(q `2).| <= |.q.| by JGRAPH_1:33;

per cases ( r <= 0 or r > 0 ) ;

suppose r <= 0 ; :: thesis: not |.q.| < r

hence not |.q.| < r ; :: thesis: verum

end;

suppose A11: r > 0 ; :: thesis: not |.q.| < r

q `2 = min ((- r),((G * (1,1)) `2)) by EUCLID:52;
then A12: |.(- r).| <= |.(q `2).| by A11, TOPREAL6:3, XXREAL_0:17;
- (- r) > 0 by A11;
then - r < 0 ;
then - (- r) <= |.(q `2).| by A12, ABSVALUE:def 1;
hence not |.q.| < r by A10, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence not cell (G,i,0) is bounded by JORDAN2C:34; :: thesis: verum

end;

suppose i = len G ; :: thesis: not cell (G,i,0) is bounded

then A13: cell (G,i,0) = { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & s <= (G * (1,1)) `2 ) } by GOBRD11:27;
for r being Real ex q being Point of (TOP-REAL 2) st
( q in cell (G,i,0) & not |.q.| < r )

proof

let r be Real; :: thesis: ex q being Point of (TOP-REAL 2) st
( q in cell (G,i,0) & not |.q.| < r )
take q = |[(max (r,((G * ((len G),1)) `1))),((G * (1,1)) `2)]|; :: thesis: ( q in cell (G,i,0) & not |.q.| < r )
A14: |.(q `1).| <= |.q.| by JGRAPH_1:33;
(G * ((len G),1)) `1 <= max (r,((G * ((len G),1)) `1)) by XXREAL_0:25;
hence q in cell (G,i,0) by A13; :: thesis: not |.q.| < r

per cases ( r <= 0 or r > 0 ) ;

suppose r <= 0 ; :: thesis: not |.q.| < r

hence not |.q.| < r ; :: thesis: verum

end;

suppose A15: r > 0 ; :: thesis: not |.q.| < r

q `1 = max (r,((G * ((len G),1)) `1)) by EUCLID:52;
then r <= q `1 by XXREAL_0:25;
then r <= |.(q `1).| by A15, ABSVALUE:def 1;
hence not |.q.| < r by A14, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence not cell (G,i,0) is bounded by JORDAN2C:34; :: thesis: verum

end;

end;