let n be 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 :: thesis: (a + 1) * (1.REAL n) in { q where q is Point of (TOP-REAL n) : |.q.| > a }

( |.(a + 1).| >= 0 & sqrt 1 <= sqrt n ) by A1, COMPLEX1:46, SQUARE_1:26;
then A2: |.(a + 1).| * 1 <= |.(a + 1).| * (sqrt n) by XREAL_1:64;
A3: a + 1 <= |.(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)).| = |.(a + 1).| * |.(1.REAL n).| by TOPRNS_1:7
.= |.(a + 1).| * (sqrt n) by EUCLID:73 ;
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