let i, j be Nat; :: thesis: for G being Go-board st i <= len G & j <= width G holds
cell (G,i,j) = Cl (Int (cell (G,i,j)))
let G be Go-board; :: thesis: ( i <= len G & j <= width G implies cell (G,i,j) = Cl (Int (cell (G,i,j))) )
set Y = Int (cell (G,i,j));
assume A1: ( i <= len G & j <= width G ) ; :: thesis: cell (G,i,j) = Cl (Int (cell (G,i,j)))
A2: cell (G,i,j) c= Cl (Int (cell (G,i,j)))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in cell (G,i,j) or x in Cl (Int (cell (G,i,j))) )
assume A3: x in cell (G,i,j) ; :: thesis: x in Cl (Int (cell (G,i,j)))
then reconsider p = x as Point of (TOP-REAL 2) ;
for G0 being Subset of (TOP-REAL 2) st G0 is open & p in G0 holds
Int (cell (G,i,j)) meets G0
proof
let G0 be Subset of (TOP-REAL 2); :: thesis: ( G0 is open & p in G0 implies Int (cell (G,i,j)) meets G0 )
assume A4: G0 is open ; :: thesis: ( not p in G0 or Int (cell (G,i,j)) meets G0 )
now :: thesis: ( p in G0 implies (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) )
reconsider u = p as Point of (Euclid 2) by EUCLID:22;
assume A5: p in G0 ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
A6: ( j = 0 or 0 + 1 <= j ) by NAT_1:13;
reconsider v = u as Element of REAL 2 ;
A7: TopSpaceMetr (Euclid 2) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) by EUCLID:def 8;
then reconsider G00 = G0 as Subset of (TopSpaceMetr (Euclid 2)) ;
G00 is open by A4, A7, PRE_TOPC:30;
then consider r being Real such that
A8: r > 0 and
A9: Ball (u,r) c= G00 by A5, TOPMETR:15;
reconsider r = r as Real ;
A10: ( i = 0 or 0 + 1 <= i ) by NAT_1:13;
now :: thesis: ( ( i = 0 & j = 0 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( i = 0 & j = width G & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( i = 0 & 1 <= j & j < width G & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( i = len G & j = 0 & (Int (cell (G,i,j))) /\ G0 <> {} ) or ( i = len G & j = width G & (Int (cell (G,i,j))) /\ G0 <> {} ) or ( i = len G & 1 <= j & j < width G & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( 1 <= i & i < len G & j = 0 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( 1 <= i & i < len G & j = width G & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( 1 <= i & i < len G & 1 <= j & j < width G & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) )
per cases ( ( i = 0 & j = 0 ) or ( i = 0 & j = width G ) or ( i = 0 & 1 <= j & j < width G ) or ( i = len G & j = 0 ) or ( i = len G & j = width G ) or ( i = len G & 1 <= j & j < width G ) or ( 1 <= i & i < len G & j = 0 ) or ( 1 <= i & i < len G & j = width G ) or ( 1 <= i & i < len G & 1 <= j & j < width G ) ) by A1, A10, A6, XXREAL_0:1;
case A11: ( i = 0 & j = 0 ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
then p in { |[r2,s2]| where r2, s2 is Real : ( r2 <= (G * (1,1)) `1 & s2 <= (G * (1,1)) `2 ) } by A3, Th24;
then consider r2, s2 being Real such that
A12: p = |[r2,s2]| and
A13: r2 <= (G * (1,1)) `1 and
A14: s2 <= (G * (1,1)) `2 ;
set r3 = r2 - (r / 2);
set s3 = s2 - (r / 2);
A15: r * (2 ") > 0 by A8, XREAL_1:129;
then s2 - (r / 2) < (s2 - (r / 2)) + (r / 2) by XREAL_1:29;
then A16: s2 - (r / 2) < (G * (1,1)) `2 by A14, XXREAL_0:2;
reconsider q0 = |[(r2 - (r / 2)),(s2 - (r / 2))]| as Point of (TOP-REAL 2) ;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
r2 - (r / 2) < (r2 - (r / 2)) + (r / 2) by A15, XREAL_1:29;
then r2 - (r / 2) < (G * (1,1)) `1 by A13, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 < (G * (1,1)) `1 & s1 < (G * (1,1)) `2 ) } by A16;
then A17: u0 in Int (cell (G,i,j)) by A11, GOBOARD6:18;
reconsider v0 = u0 as Element of REAL 2 ;
A18: ( q0 `1 = r2 - (r / 2) & q0 `2 = s2 - (r / 2) ) by EUCLID:52;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A19: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then A20: sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
A21: ( r2 - (r2 - (r / 2)) = r / 2 & s2 - (s2 - (r / 2)) = r / 2 ) ;
( p `1 = r2 & p `2 = s2 ) by A12, EUCLID:52;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & (Pitag_dist 2) . (v,v0) < r ) by A18, A21, A19, A20, METRIC_1:def 1, TOPREAL3:7;
then u0 in Ball (u,r) by METRIC_1:11;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A17, XBOOLE_0:def 4; :: thesis: verum
end;
case A22: ( i = 0 & j = width G ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
then p in { |[r2,s2]| where r2, s2 is Real : ( r2 <= (G * (1,1)) `1 & (G * (1,(width G))) `2 <= s2 ) } by A3, Th25;
then consider r2, s2 being Real such that
A23: p = |[r2,s2]| and
A24: r2 <= (G * (1,1)) `1 and
A25: (G * (1,(width G))) `2 <= s2 ;
set r3 = r2 - (r / 2);
set s3 = s2 + (r / 2);
A26: r * (2 ") > 0 by A8, XREAL_1:129;
then s2 + (r / 2) > s2 by XREAL_1:29;
then A27: s2 + (r / 2) > (G * (1,(width G))) `2 by A25, XXREAL_0:2;
reconsider q0 = |[(r2 - (r / 2)),(s2 + (r / 2))]| as Point of (TOP-REAL 2) ;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
r2 - (r / 2) < (r2 - (r / 2)) + (r / 2) by A26, XREAL_1:29;
then r2 - (r / 2) < (G * (1,1)) `1 by A24, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 < (G * (1,1)) `1 & (G * (1,(width G))) `2 < s1 ) } by A27;
then A28: u0 in Int (cell (G,i,j)) by A22, GOBOARD6:19;
reconsider v0 = u0 as Element of REAL 2 ;
A29: ( q0 `1 = r2 - (r / 2) & q0 `2 = s2 + (r / 2) ) by EUCLID:52;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A30: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then A31: ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - (r2 - (r / 2))) ^2) + ((s2 - (s2 + (r / 2))) ^2)) < r ) by A8, A30, Lm1, METRIC_1:def 1, SQUARE_1:22;
( p `1 = r2 & p `2 = s2 ) by A23, EUCLID:52;
then dist (u,u0) < r by A29, A31, TOPREAL3:7;
then u0 in Ball (u,r) by METRIC_1:11;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A28, XBOOLE_0:def 4; :: thesis: verum
end;
case A32: ( i = 0 & 1 <= j & j < width G ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
then p in { |[r2,s2]| where r2, s2 is Real : ( r2 <= (G * (1,1)) `1 & (G * (1,j)) `2 <= s2 & s2 <= (G * (1,(j + 1))) `2 ) } by A3, Th26;
then consider r2, s2 being Real such that
A33: p = |[r2,s2]| and
A34: r2 <= (G * (1,1)) `1 and
A35: (G * (1,j)) `2 <= s2 and
A36: s2 <= (G * (1,(j + 1))) `2 ;
now :: thesis: ( ( s2 = (G * (1,j)) `2 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 & (Int (cell (G,i,j))) /\ G0 <> {} ) or ( s2 = (G * (1,(j + 1))) `2 & (Int (cell (G,i,j))) /\ G0 <> {} ) )
per cases ( s2 = (G * (1,j)) `2 or ( (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) or s2 = (G * (1,(j + 1))) `2 ) by A35, A36, XXREAL_0:1;
case A37: s2 = (G * (1,j)) `2 ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
A38: ( p `1 = r2 & p `2 = s2 ) by A33, EUCLID:52;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A39: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then A40: sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
set rl = ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2);
set rm = min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)));
set r3 = r2 - (r / 2);
set s3 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2);
set q0 = |[(r2 - (r / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]|;
A41: ( |[(r2 - (r / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| `1 = r2 - (r / 2) & |[(r2 - (r / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| `2 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) by EUCLID:52;
reconsider u0 = |[(r2 - (r / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (Euclid 2) by EUCLID:22;
reconsider v0 = u0 as Element of REAL 2 ;
A42: 1 <= len G by Th34;
( j < j + 1 & j + 1 <= width G ) by A32, NAT_1:13;
then (G * (1,j)) `2 < (G * (1,(j + 1))) `2 by A32, A42, GOBOARD5:4;
then A43: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50;
then A44: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21;
then s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > s2 by XREAL_1:29, XREAL_1:139;
then A45: s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A35, XXREAL_0:2;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 <= (r / 2) ^2 by A44, SQUARE_1:15;
then A46: ((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:7;
( 0 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 & 0 <= (r / 2) ^2 ) by XREAL_1:63;
then sqrt (((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A46, SQUARE_1:26;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - (r2 - (r / 2))) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) < r ) by A39, A40, METRIC_1:def 1, XXREAL_0:2;
then dist (u,u0) < r by A38, A41, TOPREAL3:7;
then A47: u0 in Ball (u,r) by METRIC_1:11;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17;
then A48: ((G * (1,j)) `2) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) <= ((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by XREAL_1:6;
r * (2 ") > 0 by A8, XREAL_1:129;
then r2 - (r / 2) < (r2 - (r / 2)) + (r / 2) by XREAL_1:29;
then A49: r2 - (r / 2) < (G * (1,1)) `1 by A34, XXREAL_0:2;
((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) < (((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by A43, XREAL_1:29, XREAL_1:139;
then s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A37, A48, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 < (G * (1,1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A49, A45;
then u0 in Int (cell (G,i,j)) by A32, GOBOARD6:20;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A47, XBOOLE_0:def 4; :: thesis: verum
end;
case A50: ( (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {}
set r3 = r2 - (r / 2);
set s3 = s2;
reconsider q0 = |[(r2 - (r / 2)),s2]| as Point of (TOP-REAL 2) ;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
r * (2 ") > 0 by A8, XREAL_1:129;
then r2 - (r / 2) < (r2 - (r / 2)) + (r / 2) by XREAL_1:29;
then r2 - (r / 2) < (G * (1,1)) `1 by A34, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 < (G * (1,1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A50;
then A51: u0 in Int (cell (G,i,j)) by A32, GOBOARD6:20;
reconsider v0 = u0 as Element of REAL 2 ;
A52: ( q0 `1 = r2 - (r / 2) & q0 `2 = s2 ) by EUCLID:52;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A53: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
A54: (r / 2) ^2 >= 0 by XREAL_1:63;
then ((r / 2) ^2) + 0 <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:6;
then A55: sqrt (((r / 2) ^2) + (0 ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A54, SQUARE_1:26;
A56: ( p `1 = r2 & p `2 = s2 ) by A33, EUCLID:52;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - (r2 - (r / 2))) ^2) + ((s2 - s2) ^2)) < r ) by A53, A55, METRIC_1:def 1, XXREAL_0:2;
then dist (u,u0) < r by A56, A52, TOPREAL3:7;
then u0 in Ball (u,r) by METRIC_1:11;
hence (Int (cell (G,i,j))) /\ G0 <> {} by A9, A51, XBOOLE_0:def 4; :: thesis: verum
end;
case A57: s2 = (G * (1,(j + 1))) `2 ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {}
A58: ( p `1 = r2 & p `2 = s2 ) by A33, EUCLID:52;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A59: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then A60: sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
set rl = ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2);
set rm = min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)));
set r3 = r2 - (r / 2);
set s3 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2);
reconsider q0 = |[(r2 - (r / 2)),(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (TOP-REAL 2) ;
A61: ( q0 `1 = r2 - (r / 2) & q0 `2 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) by EUCLID:52;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
reconsider v0 = u0 as Element of REAL 2 ;
A62: 1 <= len G by Th34;
( j < j + 1 & j + 1 <= width G ) by A32, NAT_1:13;
then (G * (1,j)) `2 < (G * (1,(j + 1))) `2 by A32, A62, GOBOARD5:4;
then A63: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50;
then A64: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21;
then s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) by XREAL_1:29, XREAL_1:139;
then A65: s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A36, XXREAL_0:2;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 <= (r / 2) ^2 by A64, SQUARE_1:15;
then A66: ((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:7;
( 0 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 & 0 <= (r / 2) ^2 ) by XREAL_1:63;
then sqrt (((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A66, SQUARE_1:26;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - (r2 - (r / 2))) ^2) + ((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) < r ) by A59, A60, METRIC_1:def 1, XXREAL_0:2;
then dist (u,u0) < r by A58, A61, TOPREAL3:7;
then A67: u0 in Ball (u,r) by METRIC_1:11;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17;
then A68: ((G * (1,(j + 1))) `2) - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) >= ((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by XREAL_1:10;
r * (2 ") > 0 by A8, XREAL_1:129;
then r2 - (r / 2) < (r2 - (r / 2)) + (r / 2) by XREAL_1:29;
then A69: r2 - (r / 2) < (G * (1,1)) `1 by A34, XXREAL_0:2;
((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) > (((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by A63, XREAL_1:44, XREAL_1:139;
then s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A57, A68, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 < (G * (1,1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A69, A65;
then u0 in Int (cell (G,i,j)) by A32, GOBOARD6:20;
hence (Int (cell (G,i,j))) /\ G0 <> {} by A9, A67, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ; :: thesis: verum
end;
case A70: ( i = len G & j = 0 ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {}
then p in { |[r2,s2]| where r2, s2 is Real : ( r2 >= (G * ((len G),1)) `1 & (G * (1,1)) `2 >= s2 ) } by A3, Th27;
then consider r2, s2 being Real such that
A71: p = |[r2,s2]| and
A72: r2 >= (G * ((len G),1)) `1 and
A73: (G * (1,1)) `2 >= s2 ;
set r3 = r2 + (r / 2);
set s3 = s2 - (r / 2);
A74: r * (2 ") > 0 by A8, XREAL_1:129;
then r2 + (r / 2) > r2 by XREAL_1:29;
then A75: r2 + (r / 2) > (G * ((len G),1)) `1 by A72, XXREAL_0:2;
reconsider q0 = |[(r2 + (r / 2)),(s2 - (r / 2))]| as Point of (TOP-REAL 2) ;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
s2 - (r / 2) < (s2 - (r / 2)) + (r / 2) by A74, XREAL_1:29;
then s2 - (r / 2) < (G * (1,1)) `2 by A73, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 > (G * ((len G),1)) `1 & (G * (1,1)) `2 > s1 ) } by A75;
then A76: u0 in Int (cell (G,i,j)) by A70, GOBOARD6:21;
reconsider v0 = u0 as Element of REAL 2 ;
A77: ( q0 `1 = r2 + (r / 2) & q0 `2 = s2 - (r / 2) ) by EUCLID:52;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A78: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then A79: ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - (r2 + (r / 2))) ^2) + ((s2 - (s2 - (r / 2))) ^2)) < r ) by A8, A78, Lm1, METRIC_1:def 1, SQUARE_1:22;
( p `1 = r2 & p `2 = s2 ) by A71, EUCLID:52;
then dist (u,u0) < r by A77, A79, TOPREAL3:7;
then u0 in Ball (u,r) by METRIC_1:11;
hence (Int (cell (G,i,j))) /\ G0 <> {} by A9, A76, XBOOLE_0:def 4; :: thesis: verum
end;
case A80: ( i = len G & j = width G ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {}
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A81: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then A82: sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
p in { |[r2,s2]| where r2, s2 is Real : ( (G * ((len G),1)) `1 <= r2 & (G * (1,(width G))) `2 <= s2 ) } by A3, A80, Th28;
then consider r2, s2 being Real such that
A83: p = |[r2,s2]| and
A84: (G * ((len G),1)) `1 <= r2 and
A85: (G * (1,(width G))) `2 <= s2 ;
set r3 = r2 + (r / 2);
set s3 = s2 + (r / 2);
A86: r * (2 ") > 0 by A8, XREAL_1:129;
then s2 < s2 + (r / 2) by XREAL_1:29;
then A87: s2 + (r / 2) > (G * (1,(width G))) `2 by A85, XXREAL_0:2;
reconsider q0 = |[(r2 + (r / 2)),(s2 + (r / 2))]| as Point of (TOP-REAL 2) ;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
r2 < r2 + (r / 2) by A86, XREAL_1:29;
then r2 + (r / 2) > (G * ((len G),1)) `1 by A84, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 > (G * ((len G),1)) `1 & s1 > (G * (1,(width G))) `2 ) } by A87;
then A88: u0 in Int (cell (G,i,j)) by A80, GOBOARD6:22;
reconsider v0 = u0 as Element of REAL 2 ;
A89: ( q0 `1 = r2 + (r / 2) & q0 `2 = s2 + (r / 2) ) by EUCLID:52;
A90: ( (- (r / 2)) ^2 = (r / 2) ^2 & dist (u,u0) = (Pitag_dist 2) . (v,v0) ) by METRIC_1:def 1;
A91: ( r2 - (r2 + (r / 2)) = - (r / 2) & s2 - (s2 + (r / 2)) = - (r / 2) ) ;
( p `1 = r2 & p `2 = s2 ) by A83, EUCLID:52;
then dist (u,u0) < r by A89, A91, A90, A81, A82, TOPREAL3:7;
then u0 in Ball (u,r) by METRIC_1:11;
hence (Int (cell (G,i,j))) /\ G0 <> {} by A9, A88, XBOOLE_0:def 4; :: thesis: verum
end;
case A92: ( i = len G & 1 <= j & j < width G ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
then p in { |[r2,s2]| where r2, s2 is Real : ( r2 >= (G * ((len G),1)) `1 & (G * (1,j)) `2 <= s2 & s2 <= (G * (1,(j + 1))) `2 ) } by A3, Th29;
then consider r2, s2 being Real such that
A93: p = |[r2,s2]| and
A94: r2 >= (G * ((len G),1)) `1 and
A95: (G * (1,j)) `2 <= s2 and
A96: s2 <= (G * (1,(j + 1))) `2 ;
now :: thesis: ( ( s2 = (G * (1,j)) `2 & (Int (cell (G,i,j))) /\ G0 <> {} ) or ( (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 & (Int (cell (G,i,j))) /\ G0 <> {} ) or ( s2 = (G * (1,(j + 1))) `2 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) )
per cases ( s2 = (G * (1,j)) `2 or ( (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) or s2 = (G * (1,(j + 1))) `2 ) by A95, A96, XXREAL_0:1;
case A97: s2 = (G * (1,j)) `2 ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {}
A98: ( p `1 = r2 & p `2 = s2 ) by A93, EUCLID:52;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A99: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then A100: sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
set rl = ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2);
set rm = min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)));
set r3 = r2 + (r / 2);
set s3 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2);
reconsider q0 = |[(r2 + (r / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (TOP-REAL 2) ;
A101: ( q0 `1 = r2 + (r / 2) & q0 `2 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) by EUCLID:52;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
reconsider v0 = u0 as Element of REAL 2 ;
A102: 1 <= len G by Th34;
( j < j + 1 & j + 1 <= width G ) by A92, NAT_1:13;
then (G * (1,j)) `2 < (G * (1,(j + 1))) `2 by A92, A102, GOBOARD5:4;
then A103: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50;
then A104: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21;
then s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > s2 by XREAL_1:29, XREAL_1:139;
then A105: s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A95, XXREAL_0:2;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 <= (r / 2) ^2 by A104, SQUARE_1:15;
then A106: ((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:7;
( 0 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 & 0 <= (r / 2) ^2 ) by XREAL_1:63;
then sqrt (((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A106, SQUARE_1:26;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - (r2 + (r / 2))) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) < r ) by A99, A100, METRIC_1:def 1, XXREAL_0:2;
then dist (u,u0) < r by A98, A101, TOPREAL3:7;
then A107: u0 in Ball (u,r) by METRIC_1:11;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17;
then A108: ((G * (1,j)) `2) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) <= ((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by XREAL_1:6;
r * (2 ") > 0 by A8, XREAL_1:129;
then r2 < r2 + (r / 2) by XREAL_1:29;
then A109: r2 + (r / 2) > (G * ((len G),1)) `1 by A94, XXREAL_0:2;
((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) < (((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by A103, XREAL_1:29, XREAL_1:139;
then s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A97, A108, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 > (G * ((len G),1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A109, A105;
then u0 in Int (cell (G,i,j)) by A92, GOBOARD6:23;
hence (Int (cell (G,i,j))) /\ G0 <> {} by A9, A107, XBOOLE_0:def 4; :: thesis: verum
end;
case A110: ( (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {}
set r3 = r2 + (r / 2);
set s3 = s2;
reconsider q0 = |[(r2 + (r / 2)),s2]| as Point of (TOP-REAL 2) ;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
r * (2 ") > 0 by A8, XREAL_1:129;
then r2 < r2 + (r / 2) by XREAL_1:29;
then r2 + (r / 2) > (G * ((len G),1)) `1 by A94, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 > (G * ((len G),1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A110;
then A111: u0 in Int (cell (G,i,j)) by A92, GOBOARD6:23;
reconsider v0 = u0 as Element of REAL 2 ;
A112: ( q0 `1 = r2 + (r / 2) & q0 `2 = s2 ) by EUCLID:52;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A113: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
A114: (r / 2) ^2 >= 0 by XREAL_1:63;
then ((r / 2) ^2) + 0 <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:6;
then A115: sqrt (((r / 2) ^2) + (0 ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A114, SQUARE_1:26;
A116: ( p `1 = r2 & p `2 = s2 ) by A93, EUCLID:52;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - (r2 + (r / 2))) ^2) + ((s2 - s2) ^2)) < r ) by A113, A115, METRIC_1:def 1, XXREAL_0:2;
then dist (u,u0) < r by A116, A112, TOPREAL3:7;
then u0 in Ball (u,r) by METRIC_1:11;
hence (Int (cell (G,i,j))) /\ G0 <> {} by A9, A111, XBOOLE_0:def 4; :: thesis: verum
end;
case A117: s2 = (G * (1,(j + 1))) `2 ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
A118: ( p `1 = r2 & p `2 = s2 ) by A93, EUCLID:52;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A119: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then A120: sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
set rl = ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2);
set rm = min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)));
set r3 = r2 + (r / 2);
set s3 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2);
reconsider q0 = |[(r2 + (r / 2)),(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (TOP-REAL 2) ;
A121: ( q0 `1 = r2 + (r / 2) & q0 `2 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) by EUCLID:52;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
reconsider v0 = u0 as Element of REAL 2 ;
A122: 1 <= len G by Th34;
( j < j + 1 & j + 1 <= width G ) by A92, NAT_1:13;
then (G * (1,j)) `2 < (G * (1,(j + 1))) `2 by A92, A122, GOBOARD5:4;
then A123: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50;
then A124: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21;
then s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) by XREAL_1:29, XREAL_1:139;
then A125: s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A96, XXREAL_0:2;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 <= (r / 2) ^2 by A124, SQUARE_1:15;
then A126: ((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:7;
( 0 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 & 0 <= (r / 2) ^2 ) by XREAL_1:63;
then sqrt (((r / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A126, SQUARE_1:26;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - (r2 + (r / 2))) ^2) + ((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) < r ) by A119, A120, METRIC_1:def 1, XXREAL_0:2;
then dist (u,u0) < r by A118, A121, TOPREAL3:7;
then A127: u0 in Ball (u,r) by METRIC_1:11;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17;
then A128: ((G * (1,(j + 1))) `2) - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) >= ((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by XREAL_1:10;
r * (2 ") > 0 by A8, XREAL_1:129;
then r2 < r2 + (r / 2) by XREAL_1:29;
then A129: r2 + (r / 2) > (G * ((len G),1)) `1 by A94, XXREAL_0:2;
((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) > (((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by A123, XREAL_1:44, XREAL_1:139;
then s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A117, A128, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( r1 > (G * ((len G),1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A129, A125;
then u0 in Int (cell (G,i,j)) by A92, GOBOARD6:23;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A127, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ; :: thesis: verum
end;
case A130: ( 1 <= i & i < len G & j = 0 ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
then p in { |[r2,s2]| where r2, s2 is Real : ( (G * (i,1)) `1 <= r2 & r2 <= (G * ((i + 1),1)) `1 & s2 <= (G * (1,1)) `2 ) } by A3, Th30;
then consider r2, s2 being Real such that
A131: p = |[r2,s2]| and
A132: (G * (i,1)) `1 <= r2 and
A133: r2 <= (G * ((i + 1),1)) `1 and
A134: s2 <= (G * (1,1)) `2 ;
now :: thesis: ( ( r2 = (G * (i,1)) `1 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( r2 = (G * ((i + 1),1)) `1 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) )
per cases ( r2 = (G * (i,1)) `1 or ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 ) or r2 = (G * ((i + 1),1)) `1 ) by A132, A133, XXREAL_0:1;
case A135: r2 = (G * (i,1)) `1 ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then A136: sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
set sl = ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1);
set sm = min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)));
set s3 = s2 - (r / 2);
set r3 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2);
reconsider q0 = |[(r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 - (r / 2))]| as Point of (TOP-REAL 2) ;
A137: ( q0 `1 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 - (r / 2) ) by EUCLID:52;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
reconsider v0 = u0 as Element of REAL 2 ;
A138: 1 <= width G by Th34;
( i < i + 1 & i + 1 <= len G ) by A130, NAT_1:13;
then (G * (i,1)) `1 < (G * ((i + 1),1)) `1 by A130, A138, GOBOARD5:3;
then A139: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50;
then A140: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21;
then r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > r2 by XREAL_1:29, XREAL_1:139;
then A141: r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A132, XXREAL_0:2;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A142: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 <= (r / 2) ^2 by A140, SQUARE_1:15;
then A143: ((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:7;
( 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 & 0 <= (r / 2) ^2 ) by XREAL_1:63;
then A144: sqrt (((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A143, SQUARE_1:26;
( p `1 = r2 & p `2 = s2 ) by A131, EUCLID:52;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt ((((p `1) - (q0 `1)) ^2) + (((p `2) - (q0 `2)) ^2)) < r ) by A144, A137, A142, A136, METRIC_1:def 1, XXREAL_0:2;
then dist (u,u0) < r by TOPREAL3:7;
then A145: u0 in Ball (u,r) by METRIC_1:11;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17;
then A146: ((G * (i,1)) `1) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) <= ((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by XREAL_1:6;
r * (2 ") > 0 by A8, XREAL_1:129;
then s2 - (r / 2) < (s2 - (r / 2)) + (r / 2) by XREAL_1:29;
then A147: s2 - (r / 2) < (G * (1,1)) `2 by A134, XXREAL_0:2;
((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) < (((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by A139, XREAL_1:29, XREAL_1:139;
then r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A135, A146, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & s1 < (G * (1,1)) `2 ) } by A147, A141;
then u0 in Int (cell (G,i,j)) by A130, GOBOARD6:24;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A145, XBOOLE_0:def 4; :: thesis: verum
end;
case A148: ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
set s3 = s2 - (r / 2);
set r3 = r2;
reconsider q0 = |[r2,(s2 - (r / 2))]| as Point of (TOP-REAL 2) ;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
r * (2 ") > 0 by A8, XREAL_1:129;
then s2 - (r / 2) < (s2 - (r / 2)) + (r / 2) by XREAL_1:29;
then s2 - (r / 2) < (G * (1,1)) `2 by A134, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & s1 < (G * (1,1)) `2 ) } by A148;
then A149: u0 in Int (cell (G,i,j)) by A130, GOBOARD6:24;
reconsider v0 = u0 as Element of REAL 2 ;
A150: ( q0 `1 = r2 & q0 `2 = s2 - (r / 2) ) by EUCLID:52;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A151: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
A152: (r / 2) ^2 >= 0 by XREAL_1:63;
then (0 ^2) + ((r / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:6;
then A153: sqrt ((0 ^2) + ((r / 2) ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A152, SQUARE_1:26;
A154: ( p `1 = r2 & p `2 = s2 ) by A131, EUCLID:52;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - r2) ^2) + ((s2 - (s2 - (r / 2))) ^2)) < r ) by A151, A153, METRIC_1:def 1, XXREAL_0:2;
then dist (u,u0) < r by A154, A150, TOPREAL3:7;
then u0 in Ball (u,r) by METRIC_1:11;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A149, XBOOLE_0:def 4; :: thesis: verum
end;
case A155: r2 = (G * ((i + 1),1)) `1 ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then A156: sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
set sl = ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1);
set sm = min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)));
set s3 = s2 - (r / 2);
set r3 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2);
reconsider q0 = |[(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 - (r / 2))]| as Point of (TOP-REAL 2) ;
A157: ( q0 `1 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 - (r / 2) ) by EUCLID:52;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
reconsider v0 = u0 as Element of REAL 2 ;
A158: 1 <= width G by Th34;
( i < i + 1 & i + 1 <= len G ) by A130, NAT_1:13;
then (G * (i,1)) `1 < (G * ((i + 1),1)) `1 by A130, A158, GOBOARD5:3;
then A159: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50;
then A160: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21;
then r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) by XREAL_1:29, XREAL_1:139;
then A161: r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A133, XXREAL_0:2;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A162: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 <= (r / 2) ^2 by A160, SQUARE_1:15;
then A163: ((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:7;
( 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 & 0 <= (r / 2) ^2 ) by XREAL_1:63;
then A164: sqrt (((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A163, SQUARE_1:26;
( p `1 = r2 & p `2 = s2 ) by A131, EUCLID:52;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt ((((p `1) - (q0 `1)) ^2) + (((p `2) - (q0 `2)) ^2)) < r ) by A164, A157, A162, A156, METRIC_1:def 1, XXREAL_0:2;
then dist (u,u0) < r by TOPREAL3:7;
then A165: u0 in Ball (u,r) by METRIC_1:11;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17;
then A166: ((G * ((i + 1),1)) `1) - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) >= ((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by XREAL_1:10;
r * (2 ") > 0 by A8, XREAL_1:129;
then s2 - (r / 2) < (s2 - (r / 2)) + (r / 2) by XREAL_1:29;
then A167: s2 - (r / 2) < (G * (1,1)) `2 by A134, XXREAL_0:2;
((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) > (((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by A159, XREAL_1:44, XREAL_1:139;
then r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A155, A166, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & s1 < (G * (1,1)) `2 ) } by A167, A161;
then u0 in Int (cell (G,i,j)) by A130, GOBOARD6:24;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A165, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ; :: thesis: verum
end;
case A168: ( 1 <= i & i < len G & j = width G ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
then p in { |[r2,s2]| where r2, s2 is Real : ( (G * (i,1)) `1 <= r2 & r2 <= (G * ((i + 1),1)) `1 & s2 >= (G * (1,(width G))) `2 ) } by A3, Th31;
then consider r2, s2 being Real such that
A169: p = |[r2,s2]| and
A170: (G * (i,1)) `1 <= r2 and
A171: r2 <= (G * ((i + 1),1)) `1 and
A172: s2 >= (G * (1,(width G))) `2 ;
now :: thesis: ( ( r2 = (G * (i,1)) `1 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( r2 = (G * ((i + 1),1)) `1 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) )
per cases ( r2 = (G * (i,1)) `1 or ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 ) or r2 = (G * ((i + 1),1)) `1 ) by A170, A171, XXREAL_0:1;
case A173: r2 = (G * (i,1)) `1 ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
A174: ( p `1 = r2 & p `2 = s2 ) by A169, EUCLID:52;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A175: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then A176: sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
set rl = ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1);
set rm = min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)));
set s3 = s2 + (r / 2);
set r3 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2);
reconsider q0 = |[(r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 + (r / 2))]| as Point of (TOP-REAL 2) ;
A177: ( q0 `1 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 + (r / 2) ) by EUCLID:52;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
reconsider v0 = u0 as Element of REAL 2 ;
A178: 1 <= width G by Th34;
( i < i + 1 & i + 1 <= len G ) by A168, NAT_1:13;
then (G * (i,1)) `1 < (G * ((i + 1),1)) `1 by A168, A178, GOBOARD5:3;
then A179: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50;
then A180: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21;
then r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > r2 by XREAL_1:29, XREAL_1:139;
then A181: r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A170, XXREAL_0:2;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 <= (r / 2) ^2 by A180, SQUARE_1:15;
then A182: ((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:7;
( 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 & 0 <= (r / 2) ^2 ) by XREAL_1:63;
then sqrt (((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A182, SQUARE_1:26;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 + (r / 2))) ^2)) < r ) by A175, A176, METRIC_1:def 1, XXREAL_0:2;
then dist (u,u0) < r by A174, A177, TOPREAL3:7;
then A183: u0 in Ball (u,r) by METRIC_1:11;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17;
then A184: ((G * (i,1)) `1) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) <= ((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by XREAL_1:6;
r * (2 ") > 0 by A8, XREAL_1:129;
then s2 < s2 + (r / 2) by XREAL_1:29;
then A185: s2 + (r / 2) > (G * (1,(width G))) `2 by A172, XXREAL_0:2;
((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) < (((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by A179, XREAL_1:29, XREAL_1:139;
then r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A173, A184, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & s1 > (G * (1,(width G))) `2 ) } by A185, A181;
then u0 in Int (cell (G,i,j)) by A168, GOBOARD6:25;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A183, XBOOLE_0:def 4; :: thesis: verum
end;
case A186: ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
set s3 = s2 + (r / 2);
set r3 = r2;
reconsider q0 = |[r2,(s2 + (r / 2))]| as Point of (TOP-REAL 2) ;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
r * (2 ") > 0 by A8, XREAL_1:129;
then s2 < s2 + (r / 2) by XREAL_1:29;
then s2 + (r / 2) > (G * (1,(width G))) `2 by A172, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & s1 > (G * (1,(width G))) `2 ) } by A186;
then A187: u0 in Int (cell (G,i,j)) by A168, GOBOARD6:25;
reconsider v0 = u0 as Element of REAL 2 ;
A188: ( q0 `1 = r2 & q0 `2 = s2 + (r / 2) ) by EUCLID:52;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A189: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
A190: (r / 2) ^2 >= 0 by XREAL_1:63;
then ((r / 2) ^2) + (0 ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:6;
then A191: sqrt (((r / 2) ^2) + (0 ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A190, SQUARE_1:26;
A192: ( p `1 = r2 & p `2 = s2 ) by A169, EUCLID:52;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - r2) ^2) + ((s2 - (s2 + (r / 2))) ^2)) < r ) by A189, A191, METRIC_1:def 1, XXREAL_0:2;
then dist (u,u0) < r by A192, A188, TOPREAL3:7;
then u0 in Ball (u,r) by METRIC_1:11;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A187, XBOOLE_0:def 4; :: thesis: verum
end;
case A193: r2 = (G * ((i + 1),1)) `1 ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
A194: ( p `1 = r2 & p `2 = s2 ) by A169, EUCLID:52;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A195: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then A196: sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
set rl = ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1);
set rm = min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)));
set s3 = s2 + (r / 2);
set r3 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2);
reconsider q0 = |[(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 + (r / 2))]| as Point of (TOP-REAL 2) ;
A197: ( q0 `1 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 + (r / 2) ) by EUCLID:52;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
reconsider v0 = u0 as Element of REAL 2 ;
A198: 1 <= width G by Th34;
( i < i + 1 & i + 1 <= len G ) by A168, NAT_1:13;
then (G * (i,1)) `1 < (G * ((i + 1),1)) `1 by A168, A198, GOBOARD5:3;
then A199: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50;
then A200: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21;
then r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) by XREAL_1:29, XREAL_1:139;
then A201: r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A171, XXREAL_0:2;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 <= (r / 2) ^2 by A200, SQUARE_1:15;
then A202: ((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:7;
( 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 & 0 <= (r / 2) ^2 ) by XREAL_1:63;
then sqrt (((r / 2) ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A202, SQUARE_1:26;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 + (r / 2))) ^2)) < r ) by A195, A196, METRIC_1:def 1, XXREAL_0:2;
then dist (u,u0) < r by A194, A197, TOPREAL3:7;
then A203: u0 in Ball (u,r) by METRIC_1:11;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17;
then A204: ((G * ((i + 1),1)) `1) - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) >= ((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by XREAL_1:10;
r * (2 ") > 0 by A8, XREAL_1:129;
then s2 + (r / 2) > s2 by XREAL_1:29;
then A205: s2 + (r / 2) > (G * (1,(width G))) `2 by A172, XXREAL_0:2;
((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) > (((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by A199, XREAL_1:44, XREAL_1:139;
then r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A193, A204, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & s1 > (G * (1,(width G))) `2 ) } by A205, A201;
then u0 in Int (cell (G,i,j)) by A168, GOBOARD6:25;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A203, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ; :: thesis: verum
end;
case A206: ( 1 <= i & i < len G & 1 <= j & j < width G ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
then p in { |[r2,s2]| where r2, s2 is Real : ( (G * (i,1)) `1 <= r2 & r2 <= (G * ((i + 1),1)) `1 & (G * (1,j)) `2 <= s2 & s2 <= (G * (1,(j + 1))) `2 ) } by A3, Th32;
then consider r2, s2 being Real such that
A207: p = |[r2,s2]| and
A208: (G * (i,1)) `1 <= r2 and
A209: r2 <= (G * ((i + 1),1)) `1 and
A210: (G * (1,j)) `2 <= s2 and
A211: s2 <= (G * (1,(j + 1))) `2 ;
now :: thesis: ( ( r2 = (G * (i,1)) `1 & s2 = (G * (1,j)) `2 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( r2 = (G * (i,1)) `1 & (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( r2 = (G * (i,1)) `1 & s2 = (G * (1,(j + 1))) `2 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & s2 = (G * (1,j)) `2 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & s2 = (G * (1,(j + 1))) `2 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( r2 = (G * ((i + 1),1)) `1 & s2 = (G * (1,j)) `2 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( r2 = (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) or ( r2 = (G * ((i + 1),1)) `1 & s2 = (G * (1,(j + 1))) `2 & (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ) )
per cases ( ( r2 = (G * (i,1)) `1 & s2 = (G * (1,j)) `2 ) or ( r2 = (G * (i,1)) `1 & (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) or ( r2 = (G * (i,1)) `1 & s2 = (G * (1,(j + 1))) `2 ) or ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & s2 = (G * (1,j)) `2 ) or ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) or ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & s2 = (G * (1,(j + 1))) `2 ) or ( r2 = (G * ((i + 1),1)) `1 & s2 = (G * (1,j)) `2 ) or ( r2 = (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) or ( r2 = (G * ((i + 1),1)) `1 & s2 = (G * (1,(j + 1))) `2 ) ) by A208, A209, A210, A211, XXREAL_0:1;
case A212: ( r2 = (G * (i,1)) `1 & s2 = (G * (1,j)) `2 ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
set rl1 = ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1);
set rl = ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2);
set rm = min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)));
set rm1 = min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)));
set r3 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2);
set s3 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2);
A213: 1 <= width G by Th34;
( i < i + 1 & i + 1 <= len G ) by A206, NAT_1:13;
then (G * (i,1)) `1 < (G * ((i + 1),1)) `1 by A206, A213, GOBOARD5:3;
then A214: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50;
then A215: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21;
then r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > r2 by XREAL_1:29, XREAL_1:139;
then A216: r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A208, XXREAL_0:2;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17;
then A217: ((G * (i,1)) `1) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) <= ((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by XREAL_1:6;
((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) < (((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by A214, XREAL_1:29, XREAL_1:139;
then A218: r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A212, A217, XXREAL_0:2;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17;
then A219: ((G * (1,j)) `2) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) <= ((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by XREAL_1:6;
reconsider q0 = |[(r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (TOP-REAL 2) ;
A220: ( q0 `1 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) by EUCLID:52;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
reconsider v0 = u0 as Element of REAL 2 ;
A221: 1 <= len G by Th34;
( j < j + 1 & j + 1 <= width G ) by A206, NAT_1:13;
then (G * (1,j)) `2 < (G * (1,(j + 1))) `2 by A206, A221, GOBOARD5:4;
then A222: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50;
then A223: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21;
then s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > s2 by XREAL_1:29, XREAL_1:139;
then A224: s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A210, XXREAL_0:2;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then A225: ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 <= (r / 2) ^2 by A215, SQUARE_1:15;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 <= (r / 2) ^2 by A223, SQUARE_1:15;
then A226: (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by A225, XREAL_1:7;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A227: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then A228: sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
A229: ( p `1 = r2 & p `2 = s2 ) by A207, EUCLID:52;
( 0 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 & 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 ) by XREAL_1:63;
then sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A226, SQUARE_1:26;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) < r ) by A227, A228, METRIC_1:def 1, XXREAL_0:2;
then dist (u,u0) < r by A229, A220, TOPREAL3:7;
then A230: u0 in Ball (u,r) by METRIC_1:11;
((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) < (((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by A222, XREAL_1:29, XREAL_1:139;
then s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A212, A219, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A224, A216, A218;
then u0 in Int (cell (G,i,j)) by A206, GOBOARD6:26;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A230, XBOOLE_0:def 4; :: thesis: verum
end;
case A231: ( r2 = (G * (i,1)) `1 & (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
set s3 = s2;
set rl1 = ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1);
set rm1 = min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)));
set r3 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2);
reconsider q0 = |[(r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),s2]| as Point of (TOP-REAL 2) ;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
A232: 1 <= width G by Th34;
( i < i + 1 & i + 1 <= len G ) by A206, NAT_1:13;
then (G * (i,1)) `1 < (G * ((i + 1),1)) `1 by A206, A232, GOBOARD5:3;
then A233: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50;
then A234: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21;
then A235: r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > r2 by XREAL_1:29, XREAL_1:139;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17;
then A236: ((G * (i,1)) `1) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) <= ((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by XREAL_1:6;
((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) < (((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by A233, XREAL_1:29, XREAL_1:139;
then r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A231, A236, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A231, A235;
then A237: u0 in Int (cell (G,i,j)) by A206, GOBOARD6:26;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A238: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
reconsider v0 = u0 as Element of REAL 2 ;
A239: 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 by XREAL_1:63;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (0 ^2) <= ((r / 2) ^2) + (0 ^2) by A234, SQUARE_1:15;
then A240: sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (0 ^2)) <= sqrt (((r / 2) ^2) + (0 ^2)) by A239, SQUARE_1:26;
A241: ( q0 `1 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 ) by EUCLID:52;
A242: (r / 2) ^2 >= 0 by XREAL_1:63;
then ((r / 2) ^2) + (0 ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:6;
then A243: sqrt (((r / 2) ^2) + (0 ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A242, SQUARE_1:26;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
then sqrt (((r / 2) ^2) + (0 ^2)) < r by A238, A243, XXREAL_0:2;
then A244: ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - s2) ^2)) < r ) by A240, METRIC_1:def 1, XXREAL_0:2;
( p `1 = r2 & p `2 = s2 ) by A207, EUCLID:52;
then dist (u,u0) < r by A241, A244, TOPREAL3:7;
then u0 in Ball (u,r) by METRIC_1:11;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A237, XBOOLE_0:def 4; :: thesis: verum
end;
case A245: ( r2 = (G * (i,1)) `1 & s2 = (G * (1,(j + 1))) `2 ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
set rl1 = ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1);
set rl = ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2);
set rm = min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)));
set rm1 = min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)));
set r3 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2);
set s3 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2);
A246: 1 <= width G by Th34;
( i < i + 1 & i + 1 <= len G ) by A206, NAT_1:13;
then (G * (i,1)) `1 < (G * ((i + 1),1)) `1 by A206, A246, GOBOARD5:3;
then A247: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50;
then A248: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21;
then r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > r2 by XREAL_1:29, XREAL_1:139;
then A249: r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A208, XXREAL_0:2;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17;
then A250: ((G * (i,1)) `1) + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) <= ((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by XREAL_1:6;
((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) < (((G * (i,1)) `1) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) + ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by A247, XREAL_1:29, XREAL_1:139;
then A251: r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A245, A250, XXREAL_0:2;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17;
then A252: ((G * (1,(j + 1))) `2) - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) >= ((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by XREAL_1:13;
reconsider q0 = |[(r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (TOP-REAL 2) ;
A253: ( q0 `1 = r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) by EUCLID:52;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
reconsider v0 = u0 as Element of REAL 2 ;
A254: 1 <= len G by Th34;
( j < j + 1 & j + 1 <= width G ) by A206, NAT_1:13;
then (G * (1,j)) `2 < (G * (1,(j + 1))) `2 by A206, A254, GOBOARD5:4;
then A255: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50;
then A256: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21;
then s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < s2 by XREAL_1:44, XREAL_1:139;
then A257: s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A211, XXREAL_0:2;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then A258: ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 <= (r / 2) ^2 by A248, SQUARE_1:15;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 <= (r / 2) ^2 by A256, SQUARE_1:15;
then A259: (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by A258, XREAL_1:7;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A260: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then A261: sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
A262: ( p `1 = r2 & p `2 = s2 ) by A207, EUCLID:52;
( 0 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 & 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 ) by XREAL_1:63;
then sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A259, SQUARE_1:26;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - (r2 + ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) < r ) by A260, A261, METRIC_1:def 1, XXREAL_0:2;
then dist (u,u0) < r by A262, A253, TOPREAL3:7;
then A263: u0 in Ball (u,r) by METRIC_1:11;
((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) > (((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by A255, XREAL_1:44, XREAL_1:139;
then s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A245, A252, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A257, A249, A251;
then u0 in Int (cell (G,i,j)) by A206, GOBOARD6:26;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A263, XBOOLE_0:def 4; :: thesis: verum
end;
case A264: ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & s2 = (G * (1,j)) `2 ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
set r3 = r2;
set rl = ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2);
set rm = min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)));
set s3 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2);
reconsider q0 = |[r2,(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (TOP-REAL 2) ;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
A265: 1 <= len G by Th34;
( j < j + 1 & j + 1 <= width G ) by A206, NAT_1:13;
then (G * (1,j)) `2 < (G * (1,(j + 1))) `2 by A206, A265, GOBOARD5:4;
then A266: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50;
then A267: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21;
then A268: s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > s2 by XREAL_1:29, XREAL_1:139;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17;
then A269: ((G * (1,j)) `2) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) <= ((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by XREAL_1:6;
((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) < (((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by A266, XREAL_1:29, XREAL_1:139;
then s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A264, A269, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A264, A268;
then A270: u0 in Int (cell (G,i,j)) by A206, GOBOARD6:26;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A271: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
reconsider v0 = u0 as Element of REAL 2 ;
A272: 0 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 by XREAL_1:63;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) + (0 ^2) <= ((r / 2) ^2) + (0 ^2) by A267, SQUARE_1:15;
then A273: sqrt ((0 ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) <= sqrt ((0 ^2) + ((r / 2) ^2)) by A272, SQUARE_1:26;
A274: ( q0 `1 = r2 & q0 `2 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) by EUCLID:52;
A275: (r / 2) ^2 >= 0 by XREAL_1:63;
then (0 ^2) + ((r / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:6;
then A276: sqrt ((0 ^2) + ((r / 2) ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A275, SQUARE_1:26;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
then sqrt ((0 ^2) + ((r / 2) ^2)) < r by A271, A276, XXREAL_0:2;
then A277: ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - r2) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) < r ) by A273, METRIC_1:def 1, XXREAL_0:2;
( p `1 = r2 & p `2 = s2 ) by A207, EUCLID:52;
then dist (u,u0) < r by A274, A277, TOPREAL3:7;
then u0 in Ball (u,r) by METRIC_1:11;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A270, XBOOLE_0:def 4; :: thesis: verum
end;
case A278: ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
set s3 = s2;
set r3 = r2;
reconsider q0 = |[r2,s2]| as Point of (TOP-REAL 2) ;
A279: ( q0 `1 = r2 & q0 `2 = s2 ) by EUCLID:52;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
reconsider v0 = u0 as Element of REAL 2 ;
( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - r2) ^2) + ((s2 - s2) ^2)) < r ) by A8, METRIC_1:def 1, SQUARE_1:22;
then dist (u,u0) < r by A207, A279, TOPREAL3:7;
then A280: u0 in Ball (u,r) by METRIC_1:11;
u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A278;
then u0 in Int (cell (G,i,j)) by A206, GOBOARD6:26;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A280, XBOOLE_0:def 4; :: thesis: verum
end;
case A281: ( (G * (i,1)) `1 < r2 & r2 < (G * ((i + 1),1)) `1 & s2 = (G * (1,(j + 1))) `2 ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
set r3 = r2;
set rl = ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2);
set rm = min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)));
set s3 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2);
reconsider q0 = |[r2,(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (TOP-REAL 2) ;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
A282: 1 <= len G by Th34;
( j < j + 1 & j + 1 <= width G ) by A206, NAT_1:13;
then (G * (1,j)) `2 < (G * (1,(j + 1))) `2 by A206, A282, GOBOARD5:4;
then A283: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50;
then A284: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21;
then A285: s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < s2 by XREAL_1:44, XREAL_1:139;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17;
then A286: ((G * (1,(j + 1))) `2) - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) >= ((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by XREAL_1:13;
((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) > (((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by A283, XREAL_1:44, XREAL_1:139;
then s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A281, A286, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A281, A285;
then A287: u0 in Int (cell (G,i,j)) by A206, GOBOARD6:26;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A288: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
reconsider v0 = u0 as Element of REAL 2 ;
A289: 0 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 by XREAL_1:63;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) + (0 ^2) <= ((r / 2) ^2) + (0 ^2) by A284, SQUARE_1:15;
then A290: sqrt ((0 ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) <= sqrt ((0 ^2) + ((r / 2) ^2)) by A289, SQUARE_1:26;
A291: ( q0 `1 = r2 & q0 `2 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) by EUCLID:52;
A292: (r / 2) ^2 >= 0 by XREAL_1:63;
then 0 + ((r / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:6;
then A293: sqrt ((0 ^2) + ((r / 2) ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A292, SQUARE_1:26;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
then sqrt ((0 ^2) + ((r / 2) ^2)) < r by A288, A293, XXREAL_0:2;
then A294: ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - r2) ^2) + ((s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) < r ) by A290, METRIC_1:def 1, XXREAL_0:2;
( p `1 = r2 & p `2 = s2 ) by A207, EUCLID:52;
then dist (u,u0) < r by A291, A294, TOPREAL3:7;
then u0 in Ball (u,r) by METRIC_1:11;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A287, XBOOLE_0:def 4; :: thesis: verum
end;
case A295: ( r2 = (G * ((i + 1),1)) `1 & s2 = (G * (1,j)) `2 ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
set rl1 = ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1);
set rl = ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2);
set rm = min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)));
set rm1 = min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)));
set r3 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2);
set s3 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2);
A296: 1 <= width G by Th34;
( i < i + 1 & i + 1 <= len G ) by A206, NAT_1:13;
then (G * (i,1)) `1 < (G * ((i + 1),1)) `1 by A206, A296, GOBOARD5:3;
then A297: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50;
then A298: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21;
then r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < r2 by XREAL_1:44, XREAL_1:139;
then A299: r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A209, XXREAL_0:2;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17;
then A300: ((G * ((i + 1),1)) `1) - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) >= ((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by XREAL_1:13;
((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) > (((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by A297, XREAL_1:44, XREAL_1:139;
then A301: r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A295, A300, XXREAL_0:2;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17;
then A302: ((G * (1,j)) `2) + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) <= ((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by XREAL_1:6;
reconsider q0 = |[(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (TOP-REAL 2) ;
A303: ( q0 `1 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) by EUCLID:52;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
reconsider v0 = u0 as Element of REAL 2 ;
A304: 1 <= len G by Th34;
( j < j + 1 & j + 1 <= width G ) by A206, NAT_1:13;
then (G * (1,j)) `2 < (G * (1,(j + 1))) `2 by A206, A304, GOBOARD5:4;
then A305: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50;
then A306: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21;
then s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > s2 by XREAL_1:29, XREAL_1:139;
then A307: s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A210, XXREAL_0:2;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then A308: ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 <= (r / 2) ^2 by A298, SQUARE_1:15;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 <= (r / 2) ^2 by A306, SQUARE_1:15;
then A309: (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by A308, XREAL_1:7;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A310: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then A311: sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
A312: ( p `1 = r2 & p `2 = s2 ) by A207, EUCLID:52;
( 0 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 & 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 ) by XREAL_1:63;
then sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A309, SQUARE_1:26;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - (s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))) ^2)) < r ) by A310, A311, METRIC_1:def 1, XXREAL_0:2;
then dist (u,u0) < r by A312, A303, TOPREAL3:7;
then A313: u0 in Ball (u,r) by METRIC_1:11;
((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) < (((G * (1,j)) `2) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) + ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by A305, XREAL_1:29, XREAL_1:139;
then s2 + ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A295, A302, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A307, A299, A301;
then u0 in Int (cell (G,i,j)) by A206, GOBOARD6:26;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A313, XBOOLE_0:def 4; :: thesis: verum
end;
case A314: ( r2 = (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s2 & s2 < (G * (1,(j + 1))) `2 ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
set s3 = s2;
set rl1 = ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1);
set rm1 = min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)));
set r3 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2);
reconsider q0 = |[(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),s2]| as Point of (TOP-REAL 2) ;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
A315: 1 <= width G by Th34;
( i < i + 1 & i + 1 <= len G ) by A206, NAT_1:13;
then (G * (i,1)) `1 < (G * ((i + 1),1)) `1 by A206, A315, GOBOARD5:3;
then A316: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50;
then A317: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21;
then A318: r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < r2 by XREAL_1:44, XREAL_1:139;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17;
then A319: ((G * ((i + 1),1)) `1) - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) >= ((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by XREAL_1:13;
((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) > (((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by A316, XREAL_1:44, XREAL_1:139;
then r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A314, A319, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A314, A318;
then A320: u0 in Int (cell (G,i,j)) by A206, GOBOARD6:26;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A321: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
reconsider v0 = u0 as Element of REAL 2 ;
A322: 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 by XREAL_1:63;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then (0 ^2) + (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) <= (0 ^2) + ((r / 2) ^2) by A317, SQUARE_1:15;
then A323: sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (0 ^2)) <= sqrt (((r / 2) ^2) + (0 ^2)) by A322, SQUARE_1:26;
A324: ( q0 `1 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 ) by EUCLID:52;
A325: (r / 2) ^2 >= 0 by XREAL_1:63;
then ((r / 2) ^2) + 0 <= ((r / 2) ^2) + ((r / 2) ^2) by XREAL_1:6;
then A326: sqrt (((r / 2) ^2) + (0 ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A325, SQUARE_1:26;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
then sqrt (((r / 2) ^2) + (0 ^2)) < r by A321, A326, XXREAL_0:2;
then A327: ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt (((r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2))) ^2) + ((s2 - s2) ^2)) < r ) by A323, METRIC_1:def 1, XXREAL_0:2;
( p `1 = r2 & p `2 = s2 ) by A207, EUCLID:52;
then dist (u,u0) < r by A324, A327, TOPREAL3:7;
then u0 in Ball (u,r) by METRIC_1:11;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A320, XBOOLE_0:def 4; :: thesis: verum
end;
case A328: ( r2 = (G * ((i + 1),1)) `1 & s2 = (G * (1,(j + 1))) `2 ) ; :: thesis: (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2)
set rl1 = ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1);
set rl = ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2);
set rm = min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)));
set rm1 = min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)));
set r3 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2);
set s3 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2);
A329: 1 <= width G by Th34;
( i < i + 1 & i + 1 <= len G ) by A206, NAT_1:13;
then (G * (i,1)) `1 < (G * ((i + 1),1)) `1 by A206, A329, GOBOARD5:3;
then A330: ((G * ((i + 1),1)) `1) - ((G * (i,1)) `1) > 0 by XREAL_1:50;
then A331: min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1))) > 0 by A8, XXREAL_0:21;
then r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < r2 by XREAL_1:44, XREAL_1:139;
then A332: r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) < (G * ((i + 1),1)) `1 by A209, XXREAL_0:2;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= (((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2 by XREAL_1:72, XXREAL_0:17;
then A333: ((G * ((i + 1),1)) `1) - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) >= ((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by XREAL_1:13;
((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) > (((G * ((i + 1),1)) `1) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2)) - ((((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)) / 2) by A330, XREAL_1:44, XREAL_1:139;
then A334: r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) > (G * (i,1)) `1 by A328, A333, XXREAL_0:2;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= (((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2 by XREAL_1:72, XXREAL_0:17;
then A335: ((G * (1,(j + 1))) `2) - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) >= ((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by XREAL_1:13;
(sqrt 2) / 2 < 1 by Lm1, SQUARE_1:21, XREAL_1:189;
then A336: r * ((sqrt 2) / 2) < r * 1 by A8, XREAL_1:68;
A337: ( p `1 = r2 & p `2 = s2 ) by A207, EUCLID:52;
((r / 2) ^2) + ((r / 2) ^2) = 2 * ((r / 2) ^2)
.= ((sqrt 2) ^2) * ((r / 2) ^2) by SQUARE_1:def 2
.= ((r / 2) * (sqrt 2)) ^2 ;
then A338: sqrt (((r / 2) ^2) + ((r / 2) ^2)) = r * ((sqrt 2) / 2) by A8, Lm1, SQUARE_1:22;
A339: 1 <= len G by Th34;
(min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then A340: ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 <= (r / 2) ^2 by A331, SQUARE_1:15;
reconsider q0 = |[(r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)),(s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2))]| as Point of (TOP-REAL 2) ;
A341: ( q0 `1 = r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) & q0 `2 = s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ) by EUCLID:52;
reconsider u0 = q0 as Point of (Euclid 2) by EUCLID:22;
reconsider v0 = u0 as Element of REAL 2 ;
A342: ( r2 - (r2 - ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2)) = (min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2 & s2 - (s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2)) = (min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 ) ;
( j < j + 1 & j + 1 <= width G ) by A206, NAT_1:13;
then (G * (1,j)) `2 < (G * (1,(j + 1))) `2 by A206, A339, GOBOARD5:4;
then A343: ((G * (1,(j + 1))) `2) - ((G * (1,j)) `2) > 0 by XREAL_1:50;
then A344: min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2))) > 0 by A8, XXREAL_0:21;
then s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < s2 by XREAL_1:44, XREAL_1:139;
then A345: s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) < (G * (1,(j + 1))) `2 by A211, XXREAL_0:2;
(min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2 <= r / 2 by XREAL_1:72, XXREAL_0:17;
then ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 <= (r / 2) ^2 by A344, SQUARE_1:15;
then A346: (((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2) <= ((r / 2) ^2) + ((r / 2) ^2) by A340, XREAL_1:7;
( 0 <= ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2 & 0 <= ((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2 ) by XREAL_1:63;
then sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) <= sqrt (((r / 2) ^2) + ((r / 2) ^2)) by A346, SQUARE_1:26;
then ( dist (u,u0) = (Pitag_dist 2) . (v,v0) & sqrt ((((min (r,(((G * ((i + 1),1)) `1) - ((G * (i,1)) `1)))) / 2) ^2) + (((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) ^2)) < r ) by A336, A338, METRIC_1:def 1, XXREAL_0:2;
then dist (u,u0) < r by A337, A341, A342, TOPREAL3:7;
then A347: u0 in Ball (u,r) by METRIC_1:11;
((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) > (((G * (1,(j + 1))) `2) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2)) - ((((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)) / 2) by A343, XREAL_1:44, XREAL_1:139;
then s2 - ((min (r,(((G * (1,(j + 1))) `2) - ((G * (1,j)) `2)))) / 2) > (G * (1,j)) `2 by A328, A335, XXREAL_0:2;
then u0 in { |[r1,s1]| where r1, s1 is Real : ( (G * (i,1)) `1 < r1 & r1 < (G * ((i + 1),1)) `1 & (G * (1,j)) `2 < s1 & s1 < (G * (1,(j + 1))) `2 ) } by A345, A332, A334;
then u0 in Int (cell (G,i,j)) by A206, GOBOARD6:26;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) by A9, A347, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ; :: thesis: verum
end;
end;
end;
hence (Int (cell (G,i,j))) /\ G0 <> {} (TOP-REAL 2) ; :: thesis: verum
end;
hence ( not p in G0 or Int (cell (G,i,j)) meets G0 ) ; :: thesis: verum
end;
hence x in Cl (Int (cell (G,i,j))) by PRE_TOPC:def 7; :: thesis: verum
end;
( Cl (Int (cell (G,i,j))) c= Cl (cell (G,i,j)) & cell (G,i,j) is closed ) by Th33, PRE_TOPC:19, TOPS_1:16;
then Cl (Int (cell (G,i,j))) c= cell (G,i,j) by PRE_TOPC:22;
hence cell (G,i,j) = Cl (Int (cell (G,i,j))) by A2; :: thesis: verum