reconsider ONE = 1 as Real ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Int cb or x in Ball (p,r) )
assume x in Int cb ; :: thesis: x in Ball (p,r)
then consider Q being Subset of (TOP-REAL n) such that
A5: Q is open and
A6: Q c= cl_Ball (p,r) and
A7: x in Q by TOPS_1:22;
reconsider q = x as Point of (TOP-REAL n) by A7;
consider w being positive Real such that
A8: Ball (q,w) c= Q by A5, A7, TOPS_4:2;
assume not x in Ball (p,r) ; :: thesis: contradiction
then q in Sphere (p,r) by A3, A6, A7, XBOOLE_0:def 3;
then A9: |.(q - p).| = r by TOPREAL9:9;
set w2 = w / 2;
set wr = ((w / 2) / r) * (q - p);
A10: |.((w / 2) / r).| = (w / 2) / r by A1, ABSVALUE:def 1;
A11: ((((w / 2) / r) * (q - p)) + q) - p = (((w / 2) / r) * (q - p)) + (q - p) by RLVECT_1:28
.= (((w / 2) / r) * (q - p)) + (ONE * (q - p)) by RLVECT_1:def 8
.= (((w / 2) / r) + ONE) * (q - p) by RLVECT_1:def 6 ;
|.(((((w / 2) / r) * (q - p)) + q) - q).| = |.((((w / 2) / r) * (q - p)) + (q - q)).| by RLVECT_1:def 3
.= |.((((w / 2) / r) * (q - p)) + (0. (TOP-REAL n))).| by RLVECT_1:15
.= |.(((w / 2) / r) * (q - p)).|
.= ((w / 2) / r) * r by A9, A10, TOPRNS_1:7
.= w / 2 by A1, XCMPLX_1:87 ;
then |.(((((w / 2) / r) * (q - p)) + q) - q).| < w by XREAL_1:216;
then (((w / 2) / r) * (q - p)) + q in Ball (q,w) ;
then A12: (((w / 2) / r) * (q - p)) + q in Q by A8;
A13: ((w / 2) / r) + ONE = ((w / 2) / r) + (r / r) by A1, XCMPLX_1:60
.= ((w / 2) + r) / r ;
A14: (w / 2) + r > 0 + r by XREAL_1:6;
|.(((w / 2) + r) / r).| = ((w / 2) + r) / r by A1, ABSVALUE:def 1;
then |.(((((w / 2) / r) * (q - p)) + q) - p).| = (((w / 2) + r) / r) * r by A9, A13, A11, TOPRNS_1:7
.= (w / 2) + r by A1, XCMPLX_1:87 ;
hence contradiction by A6, A12, A14, TOPREAL9:8; :: thesis: verum