let n be Element of NAT ; :: thesis: for a being Real st n >= 1 holds
{ q where q is Point of (TOP-REAL n) : |.q.| > a } <> {}
let a be Real; :: thesis: ( n >= 1 implies { q where q is Point of (TOP-REAL n) : |.q.| > a } <> {} )
assume A1: n >= 1 ; :: thesis: { q where q is Point of (TOP-REAL n) : |.q.| > a } <> {}

now

( abs (a + 1) >= 0 & sqrt 1 <= sqrt n ) by A1, COMPLEX1:46, SQUARE_1:26;
then A2: (abs (a + 1)) * 1 <= (abs (a + 1)) * (sqrt n) by SQUARE_1:18, XREAL_1:64;
A3: a + 1 <= abs (a + 1) by ABSVALUE:4;
assume not (a + 1) * (1.REAL n) in { q where q is Point of (TOP-REAL n) : |.q.| > a } ; :: thesis: contradiction
then A4: |.((a + 1) * (1.REAL n)).| <= a ;
A5: a < a + 1 by XREAL_1:29;
|.((a + 1) * (1.REAL n)).| = (abs (a + 1)) * |.(1.REAL n).| by TOPRNS_1:7
.= (abs (a + 1)) * (sqrt n) by Th35 ;
then a + 1 <= |.((a + 1) * (1.REAL n)).| by A2, A3, XXREAL_0:2;
hence contradiction by A4, A5, XXREAL_0:2; :: thesis: verum

end;

hence { q where q is Point of (TOP-REAL n) : |.q.| > a } <> {} ; :: thesis: verum