let n be Element of NAT ; :: thesis: for A being Subset of (TOP-REAL n) st 1 <= n & A is Bounded holds
A ` <> {}
let A be Subset of (TOP-REAL n); :: thesis: ( 1 <= n & A is Bounded implies A ` <> {} )
assume A1: ( 1 <= n & A is Bounded ) ; :: thesis: A ` <> {}
then consider r being Real such that
A2: for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r by Th40;
A3: |.(r * (1.REAL n)).| = (abs r) * |.(1.REAL n).| by TOPRNS_1:8;
abs r >= 0 by COMPLEX1:132;
then A4: (abs r) * |.(1.REAL n).| >= (abs r) * 1 by A1, Th38, XREAL_1:66;
r <= abs r by ABSVALUE:11;
then not r * (1.REAL n) in A by A2, A3, A4, XXREAL_0:2;
hence A ` <> {} by XBOOLE_0:def 5; :: thesis: verum