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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of (TOP-REAL n) : |.q.| > a } or x in (REAL n) \ { q2 where q2 is Point of (TOP-REAL n) : |.q2.| < a } )
assume x in { q where q is Point of (TOP-REAL n) : |.q.| > a } ; :: thesis: x in (REAL n) \ { q2 where q2 is Point of (TOP-REAL n) : |.q2.| < a }
then consider q being Point of (TOP-REAL n) such that
A2: q = x and
A3: |.q.| > a ;

A4: now :: thesis: not x in { q2 where q2 is Point of (TOP-REAL n) : |.q2.| < a }

assume x in { q2 where q2 is Point of (TOP-REAL n) : |.q2.| < a } ; :: thesis: contradiction
then ex q2 being Point of (TOP-REAL n) st
( q2 = x & |.q2.| < a ) ;
hence contradiction by A2, A3; :: thesis: verum

end;

q in the carrier of (TOP-REAL n) ;
then q in REAL n by EUCLID:22;
hence x in (REAL n) \ { q2 where q2 is Point of (TOP-REAL n) : |.q2.| < a } by A2, A4, XBOOLE_0:def 5; :: thesis: verum

end;

assume n >= 1 ; :: thesis: (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } <> {}
hence (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < a } <> {} by A1, Th37, XBOOLE_1:3; :: thesis: verum