let n be Nat; :: thesis: for W being Subset of (Euclid n)
for a being Real st n >= 2 & W = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
not W is bounded
let W be Subset of (Euclid n); :: thesis: for a being Real st n >= 2 & W = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
not W is bounded
let a be Real; :: thesis: ( n >= 2 & W = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } implies 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 } ) ; :: 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 ;
A4: 0 <= |.a.| by COMPLEX1:46;
then A5: (r + |.a.|) + 0 < (r + |.a.|) + (r + |.a.|) by A2, XREAL_1:6;
n >= 1 by A1, XXREAL_0:2;
then A6: 1 <= sqrt n by SQUARE_1:18, SQUARE_1:26;

A7: now :: thesis: not - ((r + |.a.|) * (1.REAL n)) in { q where q is Point of (TOP-REAL n) : |.q.| < a }

( a <= |.a.| & |.a.| < r + |.a.| ) by A2, ABSVALUE:4, XREAL_1:29;
then A8: a < r + |.a.| by XXREAL_0:2;
assume - ((r + |.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 + |.a.|) * (1.REAL n)) & |.q.| < a ) ;
|.(r + |.a.|).| >= 0 by COMPLEX1:46;
then A10: |.(r + |.a.|).| * 1 <= |.(r + |.a.|).| * (sqrt n) by A6, XREAL_1:64;
A11: r + |.a.| <= |.(r + |.a.|).| by ABSVALUE:4;
|.(- ((r + |.a.|) * (1.REAL n))).| = |.((r + |.a.|) * (1.REAL n)).| by TOPRNS_1:26
.= |.(r + |.a.|).| * |.(1.REAL n).| by TOPRNS_1:7
.= |.(r + |.a.|).| * (sqrt n) by EUCLID:73 ;
then r + |.a.| <= |.(- ((r + |.a.|) * (1.REAL n))).| by A10, A11, XXREAL_0:2;
hence contradiction by A9, A8, XXREAL_0:2; :: thesis: verum

end;

A12: now :: thesis: not (r + |.a.|) * (1.REAL n) in { q where q is Point of (TOP-REAL n) : |.q.| < a }

( a <= |.a.| & |.a.| < r + |.a.| ) by A2, ABSVALUE:4, XREAL_1:29;
then A13: a < r + |.a.| by XXREAL_0:2;
assume (r + |.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 + |.a.|) * (1.REAL n) & |.q.| < a ) ;
|.(r + |.a.|).| >= 0 by COMPLEX1:46;
then A15: |.(r + |.a.|).| * 1 <= |.(r + |.a.|).| * (sqrt n) by A6, XREAL_1:64;
A16: r + |.a.| <= |.(r + |.a.|).| by ABSVALUE:4;
|.((r + |.a.|) * (1.REAL n)).| = |.(r + |.a.|).| * |.(1.REAL n).| by TOPRNS_1:7
.= |.(r + |.a.|).| * (sqrt n) by EUCLID:73 ;
then r + |.a.| <= |.((r + |.a.|) * (1.REAL n)).| by A15, A16, XXREAL_0:2;
hence contradiction by A14, A13, XXREAL_0:2; :: thesis: verum

end;

reconsider z2 = - ((r + |.a.|) * (1.REAL n)) as Point of (Euclid n) by EUCLID:22;
reconsider z1 = (r + |.a.|) * (1.REAL n) as Point of (Euclid n) by EUCLID:22;
A17: (r + |.a.|) + (r + |.a.|) <= |.((r + |.a.|) + (r + |.a.|)).| by ABSVALUE:4;
|.((r + |.a.|) + (r + |.a.|)).| >= 0 by COMPLEX1:46;
then A18: |.((r + |.a.|) + (r + |.a.|)).| * 1 <= |.((r + |.a.|) + (r + |.a.|)).| * (sqrt n) by A6, XREAL_1:64;
dist (z1,z2) = |.(((r + |.a.|) * (1.REAL n)) - (- ((r + |.a.|) * (1.REAL n)))).| by JGRAPH_1:28
.= |.(((r + |.a.|) * 1R) + (- (- ((r + |.a.|) * 1R)))).|
.= |.(((r + |.a.|) * 1R) + ((r + |.a.|) * 1R)).|
.= |.(((r + |.a.|) + (r + |.a.|)) * 1R).| by RLVECT_1:def 6
.= |.(((r + |.a.|) + (r + |.a.|)) * (1.REAL n)).|
.= |.((r + |.a.|) + (r + |.a.|)).| * |.(1.REAL n).| by TOPRNS_1:7
.= |.((r + |.a.|) + (r + |.a.|)).| * (sqrt n) by EUCLID:73 ;
then (r + |.a.|) + (r + |.a.|) <= dist (z1,z2) by A18, A17, XXREAL_0:2;
then A19: r + |.a.| < dist (z1,z2) by A5, XXREAL_0:2;
r + 0 <= r + |.a.| by A4, XREAL_1:6;
then A20: r < dist (z1,z2) by A19, XXREAL_0:2;
- ((r + |.a.|) * (1.REAL n)) in the carrier of (TOP-REAL n) ;
then - ((r + |.a.|) * (1.REAL n)) in REAL n by EUCLID:22;
then A21: - ((r + |.a.|) * (1.REAL n)) in W by A1, A7, XBOOLE_0:def 5;
(r + |.a.|) * (1.REAL n) in the carrier of (TOP-REAL n) ;
then (r + |.a.|) * (1.REAL n) in REAL n by EUCLID:22;
then (r + |.a.|) * (1.REAL n) in W by A1, A12, XBOOLE_0:def 5;
hence contradiction by A3, A21, A20; :: thesis: verum