let G be Go-board; :: thesis: for j being Element of NAT st j <= width G holds
not cell G,0 ,j is Bounded
let j be Element of NAT ; :: thesis: ( j <= width G implies not cell G,0 ,j is Bounded )
assume A1: j <= width G ; :: thesis: not cell G,0 ,j is Bounded

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

suppose j = 0 ; :: thesis: not cell G,0 ,j is Bounded

then A2: cell G,0 ,j = { |[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,0 ,j & not |.q.| < r )

proof

let r be Real; :: thesis: ex q being Point of (TOP-REAL 2) st
( q in cell G,0 ,j & not |.q.| < r )
take q = |[(min (- r),((G * 1,1) `1 )),(min (- r),((G * 1,1) `2 ))]|; :: thesis: ( q in cell G,0 ,j & not |.q.| < r )
( 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,0 ,j by A2; :: thesis: not |.q.| < r
A3: abs (q `1 ) <= |.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 r > 0 ; :: thesis: not |.q.| < r

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

end;

end;

end;

hence not cell G,0 ,j is Bounded by JORDAN2C:40; :: thesis: verum

end;

suppose A5: ( j >= 1 & j < width G ) ; :: thesis: not cell G,0 ,j is Bounded

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

proof

let r be Real; :: thesis: ex q being Point of (TOP-REAL 2) st
( q in cell G,0 ,j & not |.q.| < r )
take q = |[(min (- r),((G * 1,1) `1 )),((G * 1,j) `2 )]|; :: thesis: ( q in cell G,0 ,j & not |.q.| < r )
len G <> 0 by GOBOARD1:def 5;
then A7: 1 <= len G by NAT_1:14;
( j < j + 1 & j + 1 <= width G ) by A5, NAT_1:13;
then A8: (G * 1,j) `2 <= (G * 1,(j + 1)) `2 by A5, A7, GOBOARD5:5;
min (- r),((G * 1,1) `1 ) <= (G * 1,1) `1 by XXREAL_0:17;
hence q in cell G,0 ,j by A6, A8; :: thesis: not |.q.| < r
A9: abs (q `1 ) <= |.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 r > 0 ; :: thesis: not |.q.| < r

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

end;

end;

end;

hence not cell G,0 ,j is Bounded by JORDAN2C:40; :: thesis: verum

end;

suppose j = width G ; :: thesis: not cell G,0 ,j is Bounded

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

proof

let r be Real; :: thesis: ex q being Point of (TOP-REAL 2) st
( q in cell G,0 ,j & not |.q.| < r )
take q = |[((G * 1,1) `1 ),(max r,((G * 1,(width G)) `2 ))]|; :: thesis: ( q in cell G,0 ,j & not |.q.| < r )
(G * 1,(width G)) `2 <= max r,((G * 1,(width G)) `2 ) by XXREAL_0:25;
hence q in cell G,0 ,j by A11; :: thesis: not |.q.| < r
A12: 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 A13: r > 0 ; :: thesis: not |.q.| < r

q `2 = max r,((G * 1,(width G)) `2 ) by EUCLID:56;
then r <= q `2 by XXREAL_0:25;
then r <= abs (q `2 ) by A13, ABSVALUE:def 1;
hence not |.q.| < r by A12, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence not cell G,0 ,j is Bounded by JORDAN2C:40; :: thesis: verum

end;

end;