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:132, SQUARE_1:94;
then A2: (abs (a + 1)) * 1 <= (abs (a + 1)) * (sqrt n) by SQUARE_1:83, XREAL_1:66;
A3: a + 1 <= abs (a + 1) by ABSVALUE:11;
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:31;
|.((a + 1) * (1.REAL n)).| = (abs (a + 1)) * |.(1.REAL n).| by TOPRNS_1:8
.= (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