let n be 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 that
A1: 1 <= n and
A2: A is bounded ; :: thesis: A ` <> {}
consider r being Real such that
A3: for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r by A2, Th21;
|.r.| >= 0 by COMPLEX1:46;
then A4: |.r.| * |.(1.REAL n).| >= |.r.| * 1 by A1, EUCLID:75, XREAL_1:64;
( |.(r * (1.REAL n)).| = |.r.| * |.(1.REAL n).| & r <= |.r.| ) by ABSVALUE:4, TOPRNS_1:7;
then not r * (1.REAL n) in A by A3, A4, XXREAL_0:2;
hence A ` <> {} by XBOOLE_0:def 5; :: thesis: verum