let G be Go-board; :: thesis: for j being Nat st j <= width G holds
not cell (G,0,j) is bounded

let j be 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 ;
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 () st
( q in cell (G,0,j) & not |.q.| < r )
proof
let r be Real; :: thesis: ex q being Point of () 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 )
A3: min ((- r),((G * (1,1)) `2)) <= (G * (1,1)) `2 by XXREAL_0:17;
min ((- r),((G * (1,1)) `1)) <= (G * (1,1)) `1 by XXREAL_0:17;
hence q in cell (G,0,j) by A2, A3; :: thesis: not |.q.| < r
A4: |.(q `1).| <= |.q.| by JGRAPH_1:33;
per cases ( r <= 0 or r > 0 ) ;
suppose A5: r > 0 ; :: thesis: not |.q.| < r
q `1 = min ((- r),((G * (1,1)) `1)) by EUCLID:52;
then A6: |.(- r).| <= |.(q `1).| by ;
- (- r) > 0 by A5;
then - r < 0 ;
then - (- r) <= |.(q `1).| by ;
hence not |.q.| < r by ; :: thesis: verum
end;
end;
end;
hence not cell (G,0,j) is bounded by JORDAN2C:34; :: thesis: verum
end;
suppose A7: ( j >= 1 & j < width G ) ; :: thesis: not cell (G,0,j) is bounded
then A8: cell (G,0,j) = { |[r,s]| where r, s is 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 () st
( q in cell (G,0,j) & not |.q.| < r )
proof
len G <> 0 by MATRIX_0:def 10;
then A9: 1 <= len G by NAT_1:14;
let r be Real; :: thesis: ex q being Point of () 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 )
A10: j < j + 1 by NAT_1:13;
A11: min ((- r),((G * (1,1)) `1)) <= (G * (1,1)) `1 by XXREAL_0:17;
j + 1 <= width G by ;
then (G * (1,j)) `2 <= (G * (1,(j + 1))) `2 by ;
hence q in cell (G,0,j) by ; :: thesis: not |.q.| < r
A12: |.(q `1).| <= |.q.| by JGRAPH_1:33;
per cases ( r <= 0 or r > 0 ) ;
suppose A13: r > 0 ; :: thesis: not |.q.| < r
q `1 = min ((- r),((G * (1,1)) `1)) by EUCLID:52;
then A14: |.(- r).| <= |.(q `1).| by ;
- (- r) > 0 by A13;
then - r < 0 ;
then - (- r) <= |.(q `1).| by ;
hence not |.q.| < r by ; :: thesis: verum
end;
end;
end;
hence not cell (G,0,j) is bounded by JORDAN2C:34; :: thesis: verum
end;
suppose j = width G ; :: thesis: not cell (G,0,j) is bounded
then A15: cell (G,0,j) = { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & (G * (1,())) `2 <= s ) } by GOBRD11:25;
for r being Real ex q being Point of () st
( q in cell (G,0,j) & not |.q.| < r )
proof
let r be Real; :: thesis: ex q being Point of () st
( q in cell (G,0,j) & not |.q.| < r )

take q = |[((G * (1,1)) `1),(max (r,((G * (1,())) `2)))]|; :: thesis: ( q in cell (G,0,j) & not |.q.| < r )
A16: |.(q `2).| <= |.q.| by JGRAPH_1:33;
(G * (1,())) `2 <= max (r,((G * (1,())) `2)) by XXREAL_0:25;
hence q in cell (G,0,j) by A15; :: thesis: not |.q.| < r
per cases ( r <= 0 or r > 0 ) ;
suppose A17: r > 0 ; :: thesis: not |.q.| < r
q `2 = max (r,((G * (1,())) `2)) by EUCLID:52;
then r <= q `2 by XXREAL_0:25;
then r <= |.(q `2).| by ;
hence not |.q.| < r by ; :: thesis: verum
end;
end;
end;
hence not cell (G,0,j) is bounded by JORDAN2C:34; :: thesis: verum
end;
end;