let G be Go-board; :: thesis: for i being Element of NAT st i <= width G holds
not cell G,(len G),i is Bounded
let i be Element of NAT ; :: thesis: ( i <= width G implies not cell G,(len G),i is Bounded )
assume A1: i <= width G ; :: thesis: not cell G,(len G),i is Bounded
per cases ( i = 0 or ( i >= 1 & i < width G ) or i = width G ) by A1, NAT_1:14, XXREAL_0:1;
suppose A2: i = 0 ; :: thesis: not cell G,(len G),i is Bounded
A3: cell G,(len G),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,(len G),0 & not |.q.| < r )
proof
let r be Real; :: thesis: ex q being Point of (TOP-REAL 2) st
( q in cell G,(len G),0 & not |.q.| < r )
take q = |[((G * (len G),1) `1 ),(min (- r),((G * 1,1) `2 ))]|; :: thesis: ( q in cell G,(len G),0 & not |.q.| < r )
A4: abs (q `2 ) <= |.q.| by JGRAPH_1:50;
min (- r),((G * 1,1) `2 ) <= (G * 1,1) `2 by XXREAL_0:17;
hence q in cell G,(len G),0 by A3; :: thesis: not |.q.| < r
per cases ( r <= 0 or r > 0 ) ;
suppose A5: r > 0 ; :: thesis: not |.q.| < r
q `2 = min (- r),((G * 1,1) `2 ) by EUCLID:56;
then A6: abs (- r) <= abs (q `2 ) by A5, TOPREAL6:8, XXREAL_0:17;
- (- r) > 0 by A5;
then - r < 0 ;
then - (- r) <= abs (q `2 ) by A6, ABSVALUE:def 1;
hence not |.q.| < r by A4, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence not cell G,(len G),i is Bounded by A2, JORDAN2C:40; :: thesis: verum
end;
suppose A7: ( i >= 1 & i < width G ) ; :: thesis: not cell G,(len G),i is Bounded
then A8: cell G,(len G),i = { |[r,s]| where r, s is Element of REAL : ( (G * (len G),1) `1 <= r & (G * 1,i) `2 <= s & s <= (G * 1,(i + 1)) `2 ) } by GOBRD11:29;
for r being Real ex q being Point of (TOP-REAL 2) st
( q in cell G,(len G),i & not |.q.| < r )
proof
len G <> 0 by GOBOARD1:def 5;
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,(len G),i & not |.q.| < r )
take q = |[(max r,((G * (len G),1) `1 )),((G * 1,i) `2 )]|; :: thesis: ( q in cell G,(len G),i & not |.q.| < r )
A10: i < i + 1 by NAT_1:13;
A11: max r,((G * (len G),1) `1 ) >= (G * (len G),1) `1 by XXREAL_0:25;
i + 1 <= width G by A7, NAT_1:13;
then (G * 1,i) `2 <= (G * 1,(i + 1)) `2 by A7, A9, A10, GOBOARD5:5;
hence q in cell G,(len G),i by A8, A11; :: thesis: not |.q.| < r
A12: abs (q `1 ) <= |.q.| by JGRAPH_1:50;
end;
hence not cell G,(len G),i is Bounded by JORDAN2C:40; :: thesis: verum
end;
suppose A14: i = width G ; :: thesis: not cell G,(len G),i is Bounded
A15: cell G,(len G),(width G) = { |[r,s]| where r, s is Real : ( (G * (len G),1) `1 <= r & (G * 1,(width G)) `2 <= s ) } by GOBRD11:28;
for r being Real ex q being Point of (TOP-REAL 2) st
( q in cell G,(len G),i & not |.q.| < r )
proof
let r be Real; :: thesis: ex q being Point of (TOP-REAL 2) st
( q in cell G,(len G),i & not |.q.| < r )
take q = |[((G * (len G),1) `1 ),(max r,((G * 1,(width G)) `2 ))]|; :: thesis: ( q in cell G,(len G),i & not |.q.| < r )
A16: abs (q `2 ) <= |.q.| by JGRAPH_1:50;
(G * 1,(width G)) `2 <= max r,((G * 1,(width G)) `2 ) by XXREAL_0:25;
hence q in cell G,(len G),i by A14, A15; :: thesis: not |.q.| < r
end;
hence not cell G,(len G),i is Bounded by JORDAN2C:40; :: thesis: verum
end;
end;