let n be Nat; :: thesis: for p being Point of ()
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 () st A = U holds
not Int A is empty

let p be Point of (); :: 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 () 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 () 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 () 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 () st A = U holds
not Int A is empty )

assume A2: ( U is open & not U is empty ) ; :: thesis: for A being Subset of () 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 () ;
TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
then reconsider Q = q as Point of () by TOPMETR:12;
A5: |.(q - p).| <= r by ;
U in the topology of (Tdisk (p,r)) by ;
then consider W being Subset of () such that
A6: W in the topology of () and
A7: U = W /\ ([#] (Tdisk (p,r))) by PRE_TOPC:def 4;
reconsider W = W as open Subset of () by ;
Int W = W by TOPS_1:23;
then q in Int W by ;
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 ;
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. ()) 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 ;
then A13: |.((((- ((min (s,r)) / (2 * r))) * (q - p)) + q) - q).| = ((min (s,r)) / (2 * r)) * |.(q - p).| by ;
((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
.= (min (s,r)) / 2 ;
then |.((((- ((min (s,r)) / (2 * r))) * (q - p)) + q) - q).| <= (min (s,r)) / 2 by ;
then A14: |.((((- ((min (s,r)) / (2 * r))) * (q - p)) + q) - q).| < min (s,r) by ;
min (s,r) <= s by XXREAL_0:17;
then |.((((- ((min (s,r)) / (2 * r))) * (q - p)) + q) - q).| < s by ;
then A15: ((- ((min (s,r)) / (2 * r))) * (q - p)) + q in Ball (q,s) ;
let A be Subset of (); :: 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 ;
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 ;
hence (1 - ((min (s,r)) / (2 * r))) * |.(q - p).| < r by ; :: thesis: verum
end;
end;
end;
A20: r / (2 * r) = (r / r) / 2 by XCMPLX_1:78
.= 1 / 2 by ;
(min (s,r)) / (2 * r) <= r / (2 * r) by ;
then 1 - ((min (s,r)) / (2 * r)) >= 1 - (1 / 2) by ;
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 ;
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 ;
Ball (q,s) c= W by ;
hence not Int A is empty by ; :: thesis: verum