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

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 A1, NAT_1:14, XXREAL_0:1;

end;

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 )

end;for r being Real ex q being Point of (TOP-REAL 2) st

( q in cell (G,0,j) & not |.q.| < r )

proof

hence
not cell (G,0,j) is bounded
by JORDAN2C:34; :: thesis: verum
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 )

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;

end;( 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;

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 (TOP-REAL 2) st

( q in cell (G,0,j) & not |.q.| < r )

end;for r being Real ex q being Point of (TOP-REAL 2) st

( q in cell (G,0,j) & not |.q.| < r )

proof

hence
not cell (G,0,j) is bounded
by JORDAN2C:34; :: thesis: verum
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 (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 )

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 A7, NAT_1:13;

then (G * (1,j)) `2 <= (G * (1,(j + 1))) `2 by A7, A9, A10, GOBOARD5:4;

hence q in cell (G,0,j) by A8, A11; :: thesis: not |.q.| < r

A12: |.(q `1).| <= |.q.| by JGRAPH_1:33;

end;then A9: 1 <= len G by NAT_1:14;

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 )

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 A7, NAT_1:13;

then (G * (1,j)) `2 <= (G * (1,(j + 1))) `2 by A7, A9, A10, GOBOARD5:4;

hence q in cell (G,0,j) by A8, A11; :: thesis: not |.q.| < r

A12: |.(q `1).| <= |.q.| by JGRAPH_1:33;

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

end;

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 A13, TOPREAL6:3, XXREAL_0:17;

- (- r) > 0 by A13;

then - r < 0 ;

then - (- r) <= |.(q `1).| by A14, ABSVALUE:def 1;

hence not |.q.| < r by A12, XXREAL_0:2; :: thesis: verum

end;then A14: |.(- r).| <= |.(q `1).| by A13, TOPREAL6:3, XXREAL_0:17;

- (- r) > 0 by A13;

then - r < 0 ;

then - (- r) <= |.(q `1).| by A14, ABSVALUE:def 1;

hence not |.q.| < r by A12, XXREAL_0:2; :: thesis: verum

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,(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 )

end;for r being Real ex q being Point of (TOP-REAL 2) st

( q in cell (G,0,j) & not |.q.| < r )

proof

hence
not cell (G,0,j) is bounded
by JORDAN2C:34; :: thesis: verum
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 )

A16: |.(q `2).| <= |.q.| by JGRAPH_1:33;

(G * (1,(width G))) `2 <= max (r,((G * (1,(width G))) `2)) by XXREAL_0:25;

hence q in cell (G,0,j) by A15; :: thesis: not |.q.| < r

end;( 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 )

A16: |.(q `2).| <= |.q.| by JGRAPH_1:33;

(G * (1,(width G))) `2 <= max (r,((G * (1,(width G))) `2)) by XXREAL_0:25;

hence q in cell (G,0,j) by A15; :: thesis: not |.q.| < r