let a be Real; :: thesis: for n being Element of NAT
for P being Subset of (TOP-REAL n) st n >= 1 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
not P is Bounded
let n be Element of NAT ; :: thesis: for P being Subset of (TOP-REAL n) st n >= 1 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } holds
not P is Bounded
let P be Subset of (TOP-REAL n); :: thesis: ( n >= 1 & P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } implies not P is Bounded )
assume that
A1: n >= 1 and
A2: P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } ; :: thesis: not P is Bounded

per cases ( a > 0 or a <= 0 ) ;

suppose A3: a > 0 ; :: thesis: not P is Bounded

now

consider p being Element of P;
assume P is Bounded ; :: thesis: contradiction
then consider r being Real such that
A4: for q being Point of (TOP-REAL n) st q in P holds
|.q.| < r by Th40;
A5: P <> {} by A1, A2, Th60;
then p in P ;
then reconsider p = p as Point of (TOP-REAL n) ;
A6: |.p.| < r by A4, A5;

A7: now

assume not ((a + r) + 1) * (1.REAL n) in (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } ; :: thesis: contradiction
then A8: ( not ((a + r) + 1) * (1.REAL n) in REAL n or ((a + r) + 1) * (1.REAL n) in { q where q is Point of (TOP-REAL n) : |.q.| < a } ) by XBOOLE_0:def 5;
((a + r) + 1) * (1.REAL n) in the carrier of (TOP-REAL n) ;
then A9: ex q being Point of (TOP-REAL n) st
( q = ((a + r) + 1) * (1.REAL n) & |.q.| < a ) by A8, EUCLID:25;
A10: (a + r) + 1 <= abs ((a + r) + 1) by ABSVALUE:11;
( a + r < (a + r) + 1 & a < a + r ) by A6, XREAL_1:31;
then A11: a < (a + r) + 1 by XXREAL_0:2;
( abs ((a + r) + 1) >= 0 & sqrt 1 <= sqrt n ) by A1, COMPLEX1:132, SQUARE_1:94;
then A12: (abs ((a + r) + 1)) * 1 <= (abs ((a + r) + 1)) * (sqrt n) by SQUARE_1:83, XREAL_1:66;
|.(((a + r) + 1) * (1.REAL n)).| = (abs ((a + r) + 1)) * |.(1.REAL n).| by TOPRNS_1:8
.= (abs ((a + r) + 1)) * (sqrt n) by Th35 ;
then (a + r) + 1 <= |.(((a + r) + 1) * (1.REAL n)).| by A12, A10, XXREAL_0:2;
hence contradiction by A9, A11, XXREAL_0:2; :: thesis: verum

end;

A13: (a + r) + 1 <= abs ((a + r) + 1) by ABSVALUE:11;
( abs ((a + r) + 1) >= 0 & sqrt 1 <= sqrt n ) by A1, COMPLEX1:132, SQUARE_1:94;
then A14: (abs ((a + r) + 1)) * 1 <= (abs ((a + r) + 1)) * (sqrt n) by SQUARE_1:83, XREAL_1:66;
A15: a + r < (a + r) + 1 by XREAL_1:31;
|.(((a + r) + 1) * (1.REAL n)).| = (abs ((a + r) + 1)) * |.(1.REAL n).| by TOPRNS_1:8
.= (abs ((a + r) + 1)) * (sqrt n) by Th35 ;
then (a + r) + 1 <= |.(((a + r) + 1) * (1.REAL n)).| by A14, A13, XXREAL_0:2;
then A16: a + r < |.(((a + r) + 1) * (1.REAL n)).| by A15, XXREAL_0:2;
r < r + a by A3, XREAL_1:31;
hence contradiction by A2, A4, A7, A16, XXREAL_0:2; :: thesis: verum

end;

hence not P is Bounded ; :: thesis: verum

end;

suppose A17: a <= 0 ; :: thesis: not P is Bounded

now

{ q where q is Point of (TOP-REAL n) : |.q.| < a } c= the carrier of (TOP-REAL n)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { q where q is Point of (TOP-REAL n) : |.q.| < a } or z in the carrier of (TOP-REAL n) )
assume z in { q where q is Point of (TOP-REAL n) : |.q.| < a } ; :: thesis: z in the carrier of (TOP-REAL n)
then ex q being Point of (TOP-REAL n) st
( q = z & |.q.| < a ) ;
hence z in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

then reconsider Q = { q where q is Point of (TOP-REAL n) : |.q.| < a } as Subset of (TOP-REAL n) ;
consider d being Element of Q;
assume { q where q is Point of (TOP-REAL n) : |.q.| < a } <> {} ; :: thesis: contradiction
then d in { q where q is Point of (TOP-REAL n) : |.q.| < a } ;
then ex q being Point of (TOP-REAL n) st
( q = d & |.q.| < a ) ;
hence contradiction by A17; :: thesis: verum

end;

then P = [#] (TOP-REAL n) by A2, EUCLID:25;
hence not P is Bounded by A1, Th41; :: thesis: verum

end;

end;