let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for r being Real st r > 0 holds
for U being Subset of (Tdisk (p,r)) st U is open & not U is empty holds
for A being Subset of (TOP-REAL n) st A = U holds
not Int A is empty
let p be Point of (TOP-REAL n); :: thesis: for r being Real st r > 0 holds
for U being Subset of (Tdisk (p,r)) st U is open & not U is empty holds
for A being Subset of (TOP-REAL n) st A = U holds
not Int A is empty
set TR = TOP-REAL n;
let r be Real; :: thesis: ( r > 0 implies for U being Subset of (Tdisk (p,r)) st U is open & not U is empty holds
for A being Subset of (TOP-REAL n) st A = U holds
not Int A is empty )
assume A1: r > 0 ; :: thesis: for U being Subset of (Tdisk (p,r)) st U is open & not U is empty holds
for A being Subset of (TOP-REAL n) st A = U holds
not Int A is empty
let U be Subset of (Tdisk (p,r)); :: thesis: ( U is open & not U is empty implies for A being Subset of (TOP-REAL n) st A = U holds
not Int A is empty )
assume A2: ( U is open & not U is empty ) ; :: thesis: for A being Subset of (TOP-REAL n) st A = U holds
not Int A is empty
consider q being object such that
A3: q in U by A2;
A4: [#] (Tdisk (p,r)) = cl_Ball (p,r) by PRE_TOPC:def 5;
then q in cl_Ball (p,r) by A3;
then reconsider q = q as Point of (TOP-REAL n) ;
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider Q = q as Point of (Euclid n) by TOPMETR:12;
A5: |.(q - p).| <= r by A3, A4, TOPREAL9:8;
U in the topology of (Tdisk (p,r)) by A2, PRE_TOPC:def 2;
then consider W being Subset of (TOP-REAL n) such that
A6: W in the topology of (TOP-REAL n) and
A7: U = W /\ ([#] (Tdisk (p,r))) by PRE_TOPC:def 4;
reconsider W = W as open Subset of (TOP-REAL n) by A6, PRE_TOPC:def 2;
Int W = W by TOPS_1:23;
then q in Int W by A3, A7, XBOOLE_0:def 4;
then consider s being Real such that
A8: s > 0 and
A9: Ball (Q,s) c= W by GOBOARD6:5;
set m = min (s,r);
set mr = (min (s,r)) / (2 * r);
A10: 0 < min (s,r) by A8, A1, XXREAL_0:21;
then A11: (min (s,r)) / 2 < min (s,r) by XREAL_1:216;
set qp = ((- ((min (s,r)) / (2 * r))) * (q - p)) + q;
A12: (((- ((min (s,r)) / (2 * r))) * (q - p)) + q) - q = ((- ((min (s,r)) / (2 * r))) * (q - p)) + (q - q) by RLVECT_1:def 3
.= ((- ((min (s,r)) / (2 * r))) * (q - p)) + (0. (TOP-REAL n)) by RLVECT_1:def 10
.= (- ((min (s,r)) / (2 * r))) * (q - p) by RLVECT_1:def 4 ;
|.(- ((min (s,r)) / (2 * r))).| = - (- ((min (s,r)) / (2 * r))) by A10, A1, ABSVALUE:def 1;
then A13: |.((((- ((min (s,r)) / (2 * r))) * (q - p)) + q) - q).| = ((min (s,r)) / (2 * r)) * |.(q - p).| by A12, EUCLID:11;
((min (s,r)) / (2 * r)) * r = (((min (s,r)) / 2) / r) * r by XCMPLX_1:78
.= ((min (s,r)) / 2) * (r / r)
.= ((min (s,r)) / 2) * 1 by XCMPLX_1:60, A1
.= (min (s,r)) / 2 ;
then |.((((- ((min (s,r)) / (2 * r))) * (q - p)) + q) - q).| <= (min (s,r)) / 2 by A5, XREAL_1:66, A10, A13;
then A14: |.((((- ((min (s,r)) / (2 * r))) * (q - p)) + q) - q).| < min (s,r) by A11, XXREAL_0:2;
min (s,r) <= s by XXREAL_0:17;
then |.((((- ((min (s,r)) / (2 * r))) * (q - p)) + q) - q).| < s by A14, XXREAL_0:2;
then A15: ((- ((min (s,r)) / (2 * r))) * (q - p)) + q in Ball (q,s) ;
let A be Subset of (TOP-REAL n); :: thesis: ( A = U implies not Int A is empty )
assume A16: A = U ; :: thesis: not Int A is empty
A17: Ball (p,r) c= cl_Ball (p,r) by TOPREAL9:16;
A18: (- ((min (s,r)) / (2 * r))) + 1 < 0 + 1 by XREAL_1:8, A10, A1;
A19: (1 - ((min (s,r)) / (2 * r))) * |.(q - p).| < r

proof

per cases ( |.(q - p).| = 0 or |.(q - p).| > 0 ) ;

suppose |.(q - p).| = 0 ; :: thesis: (1 - ((min (s,r)) / (2 * r))) * |.(q - p).| < r

hence (1 - ((min (s,r)) / (2 * r))) * |.(q - p).| < r by A1; :: thesis: verum

end;

suppose |.(q - p).| > 0 ; :: thesis: (1 - ((min (s,r)) / (2 * r))) * |.(q - p).| < r

then (1 - ((min (s,r)) / (2 * r))) * |.(q - p).| < 1 * |.(q - p).| by A18, XREAL_1:68;
hence (1 - ((min (s,r)) / (2 * r))) * |.(q - p).| < r by A5, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A20: r / (2 * r) = (r / r) / 2 by XCMPLX_1:78
.= 1 / 2 by XCMPLX_1:60, A1 ;
(min (s,r)) / (2 * r) <= r / (2 * r) by A1, XXREAL_0:17, XREAL_1:72;
then 1 - ((min (s,r)) / (2 * r)) >= 1 - (1 / 2) by A20, XREAL_1:10;
then A21: |.(1 - ((min (s,r)) / (2 * r))).| = 1 - ((min (s,r)) / (2 * r)) by ABSVALUE:def 1;
(((- ((min (s,r)) / (2 * r))) * (q - p)) + q) - p = ((- ((min (s,r)) / (2 * r))) * (q - p)) + (q - p) by RLVECT_1:def 3
.= ((- ((min (s,r)) / (2 * r))) * (q - p)) + (1 * (q - p)) by RLVECT_1:def 8
.= (1 - ((min (s,r)) / (2 * r))) * (q - p) by RLVECT_1:def 6 ;
then |.((((- ((min (s,r)) / (2 * r))) * (q - p)) + q) - p).| < r by A19, A21, EUCLID:11;
then ((- ((min (s,r)) / (2 * r))) * (q - p)) + q in Ball (p,r) ;
then A22: ((- ((min (s,r)) / (2 * r))) * (q - p)) + q in (Ball (q,s)) /\ (Ball (p,r)) by A15, XBOOLE_0:def 4;
Ball (q,s) c= W by A9, TOPREAL9:13;
hence not Int A is empty by A17, XBOOLE_1:27, A7, A4, A16, A22, TOPS_1:22; :: thesis: verum