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

assume not (a + 1) * (1.REAL n) in { q where q is Point of (TOP-REAL n) : |.q.| > a } ; :: thesis: contradiction
then A2: |.((a + 1) * (1.REAL n)).| <= a ;
A3: |.((a + 1) * (1.REAL n)).| = (abs (a + 1)) * |.(1.REAL n).| by TOPRNS_1:8
.= (abs (a + 1)) * (sqrt n) by Th35 ;
A4: abs (a + 1) >= 0 by COMPLEX1:132;
sqrt 1 <= sqrt n by A1, SQUARE_1:94;
then A5: (abs (a + 1)) * 1 <= (abs (a + 1)) * (sqrt n) by A4, SQUARE_1:83, XREAL_1:66;
a + 1 <= abs (a + 1) by ABSVALUE:11;
then A6: a + 1 <= |.((a + 1) * (1.REAL n)).| by A3, A5, XXREAL_0:2;
a < a + 1 by XREAL_1:31;
hence contradiction by A2, A6, XXREAL_0:2; :: thesis: verum

end;

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