let i be Element of 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: abs (q `1 ) <= |.q.| by JGRAPH_1:50;
( 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:56;
then A5: abs (- r) <= abs (q `1 ) by A4, TOPREAL6:8, XXREAL_0:17;
- (- r) > 0 by A4;
then - r < 0 ;
then - (- r) <= abs (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:40; :: 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 Element of 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 GOBOARD1:def 5;
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:4;
hence q in cell G,i,0 by A7, A8; :: thesis: not |.q.| < r
A10: abs (q `2 ) <= |.q.| by JGRAPH_1:50;

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:56;
then A12: abs (- r) <= abs (q `2 ) by A11, TOPREAL6:8, XXREAL_0:17;
- (- r) > 0 by A11;
then - r < 0 ;
then - (- r) <= abs (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:40; :: 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 Element of 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: abs (q `1 ) <= |.q.| by JGRAPH_1:50;
(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:56;
then r <= q `1 by XXREAL_0:25;
then r <= abs (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:40; :: thesis: verum

end;

end;