let n be Element of NAT ; :: thesis: for W being Subset of (Euclid n)
for a being Real
for P being Subset of (TOP-REAL n) st n >= 2 & W = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } & P = W holds
( P is connected & not W is bounded )
let W be Subset of (Euclid n); :: thesis: for a being Real
for P being Subset of (TOP-REAL n) st n >= 2 & W = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } & P = W holds
( P is connected & not W is bounded )
let a be Real; :: thesis: for P being Subset of (TOP-REAL n) st n >= 2 & W = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } & P = W holds
( P is connected & not W is bounded )
let P be Subset of (TOP-REAL n); :: thesis: ( n >= 2 & W = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } & P = W implies ( P is connected & not W is bounded ) )
reconsider 1R = 1.REAL n as Point of (TOP-REAL n) ;
assume A1: ( n >= 2 & W = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } & P = W ) ; :: thesis: ( P is connected & not W is bounded )
hence P is connected by Th61; :: thesis: not W is bounded
assume W is bounded ; :: thesis: contradiction
then consider r being Real such that
A2: 0 < r and
A3: for x, y being Point of (Euclid n) st x in W & y in W holds
dist x,y <= r by TBSP_1:def 9;
A4: 0 <= abs a by COMPLEX1:132;
then A5: (r + (abs a)) + 0 < (r + (abs a)) + (r + (abs a)) by A2, XREAL_1:8;
n >= 1 by A1, XXREAL_0:2;
then A6: 1 <= sqrt n by SQUARE_1:83, SQUARE_1:94;

A7: now

( a <= abs a & abs a < r + (abs a) ) by A2, ABSVALUE:11, XREAL_1:31;
then A8: a < r + (abs a) by XXREAL_0:2;
assume - ((r + (abs a)) * (1.REAL n)) in { q where q is Point of (TOP-REAL n) : |.q.| < a } ; :: thesis: contradiction
then A9: ex q being Point of (TOP-REAL n) st
( q = - ((r + (abs a)) * (1.REAL n)) & |.q.| < a ) ;
abs (r + (abs a)) >= 0 by COMPLEX1:132;
then A10: (abs (r + (abs a))) * 1 <= (abs (r + (abs a))) * (sqrt n) by A6, XREAL_1:66;
A11: r + (abs a) <= abs (r + (abs a)) by ABSVALUE:11;
|.(- ((r + (abs a)) * (1.REAL n))).| = |.((r + (abs a)) * (1.REAL n)).| by TOPRNS_1:27
.= (abs (r + (abs a))) * |.(1.REAL n).| by TOPRNS_1:8
.= (abs (r + (abs a))) * (sqrt n) by Th35 ;
then r + (abs a) <= |.(- ((r + (abs a)) * (1.REAL n))).| by A10, A11, XXREAL_0:2;
hence contradiction by A9, A8, XXREAL_0:2; :: thesis: verum

end;

A12: now

( a <= abs a & abs a < r + (abs a) ) by A2, ABSVALUE:11, XREAL_1:31;
then A13: a < r + (abs a) by XXREAL_0:2;
assume (r + (abs a)) * (1.REAL n) in { q where q is Point of (TOP-REAL n) : |.q.| < a } ; :: thesis: contradiction
then A14: ex q being Point of (TOP-REAL n) st
( q = (r + (abs a)) * (1.REAL n) & |.q.| < a ) ;
abs (r + (abs a)) >= 0 by COMPLEX1:132;
then A15: (abs (r + (abs a))) * 1 <= (abs (r + (abs a))) * (sqrt n) by A6, XREAL_1:66;
A16: r + (abs a) <= abs (r + (abs a)) by ABSVALUE:11;
|.((r + (abs a)) * (1.REAL n)).| = (abs (r + (abs a))) * |.(1.REAL n).| by TOPRNS_1:8
.= (abs (r + (abs a))) * (sqrt n) by Th35 ;
then r + (abs a) <= |.((r + (abs a)) * (1.REAL n)).| by A15, A16, XXREAL_0:2;
hence contradiction by A14, A13, XXREAL_0:2; :: thesis: verum

end;

reconsider z2 = - ((r + (abs a)) * (1.REAL n)) as Point of (Euclid n) by EUCLID:25;
reconsider z1 = (r + (abs a)) * (1.REAL n) as Point of (Euclid n) by EUCLID:25;
A17: (r + (abs a)) + (r + (abs a)) <= abs ((r + (abs a)) + (r + (abs a))) by ABSVALUE:11;
abs ((r + (abs a)) + (r + (abs a))) >= 0 by COMPLEX1:132;
then A18: (abs ((r + (abs a)) + (r + (abs a)))) * 1 <= (abs ((r + (abs a)) + (r + (abs a)))) * (sqrt n) by A6, XREAL_1:66;
dist z1,z2 = |.(((r + (abs a)) * (1.REAL n)) - (- ((r + (abs a)) * (1.REAL n)))).| by JGRAPH_1:45
.= |.(((r + (abs a)) * 1R) + (- (- ((r + (abs a)) * 1R)))).|
.= |.(((r + (abs a)) * 1R) + ((r + (abs a)) * 1R)).| by EUCLID:39
.= |.(((r + (abs a)) + (r + (abs a))) * 1R).| by EUCLID:37
.= |.(((r + (abs a)) + (r + (abs a))) * (1.REAL n)).|
.= (abs ((r + (abs a)) + (r + (abs a)))) * |.(1.REAL n).| by TOPRNS_1:8
.= (abs ((r + (abs a)) + (r + (abs a)))) * (sqrt n) by Th35 ;
then (r + (abs a)) + (r + (abs a)) <= dist z1,z2 by A18, A17, XXREAL_0:2;
then A19: r + (abs a) < dist z1,z2 by A5, XXREAL_0:2;
r + 0 <= r + (abs a) by A4, XREAL_1:8;
then A20: r < dist z1,z2 by A19, XXREAL_0:2;
- ((r + (abs a)) * (1.REAL n)) in the carrier of (TOP-REAL n) ;
then - ((r + (abs a)) * (1.REAL n)) in REAL n by EUCLID:25;
then A21: - ((r + (abs a)) * (1.REAL n)) in W by A1, A7, XBOOLE_0:def 5;
(r + (abs a)) * (1.REAL n) in the carrier of (TOP-REAL n) ;
then (r + (abs a)) * (1.REAL n) in REAL n by EUCLID:25;
then (r + (abs a)) * (1.REAL n) in W by A1, A12, XBOOLE_0:def 5;
hence contradiction by A3, A21, A20; :: thesis: verum