let a be Real; :: thesis: for n being 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 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 :: thesis: not P is bounded

set p = the 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 Th21;
A5: P <> {} by A1, A2, Th39;
then the Element of P in P ;
then reconsider p = the Element of P as Point of (TOP-REAL n) ;
A6: |.p.| < r by A4, A5;

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

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:22;
A10: (a + r) + 1 <= |.((a + r) + 1).| by ABSVALUE:4;
( a + r < (a + r) + 1 & a < a + r ) by A6, XREAL_1:29;
then A11: a < (a + r) + 1 by XXREAL_0:2;
( |.((a + r) + 1).| >= 0 & sqrt 1 <= sqrt n ) by A1, COMPLEX1:46, SQUARE_1:26;
then A12: |.((a + r) + 1).| * 1 <= |.((a + r) + 1).| * (sqrt n) by XREAL_1:64;
|.(((a + r) + 1) * (1.REAL n)).| = |.((a + r) + 1).| * |.(1.REAL n).| by TOPRNS_1:7
.= |.((a + r) + 1).| * (sqrt n) by EUCLID:73 ;
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 <= |.((a + r) + 1).| by ABSVALUE:4;
( |.((a + r) + 1).| >= 0 & sqrt 1 <= sqrt n ) by A1, COMPLEX1:46, SQUARE_1:26;
then A14: |.((a + r) + 1).| * 1 <= |.((a + r) + 1).| * (sqrt n) by XREAL_1:64;
A15: a + r < (a + r) + 1 by XREAL_1:29;
|.(((a + r) + 1) * (1.REAL n)).| = |.((a + r) + 1).| * |.(1.REAL n).| by TOPRNS_1:7
.= |.((a + r) + 1).| * (sqrt n) by EUCLID:73 ;
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:29;
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 :: thesis: not { q where q is Point of (TOP-REAL n) : |.q.| < a } <> {}

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

proof

let z be object ; :: 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) ;
set d = the Element of Q;
assume { q where q is Point of (TOP-REAL n) : |.q.| < a } <> {} ; :: thesis: contradiction
then the Element of Q in { q where q is Point of (TOP-REAL n) : |.q.| < a } ;
then ex q being Point of (TOP-REAL n) st
( q = the Element of Q & |.q.| < a ) ;
hence contradiction by A17; :: thesis: verum

end;

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

end;

end;