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

.= 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

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
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