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 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, Th40;
abs r >= 0 by COMPLEX1:132;
then A4: (abs r) * |.(1.REAL n).| >= (abs r) * 1 by A1, Th38, XREAL_1:66;
( |.(r * (1.REAL n)).| = (abs r) * |.(1.REAL n).| & r <= abs r ) by ABSVALUE:11, TOPRNS_1:8;
then not r * (1.REAL n) in A by A3, A4, XXREAL_0:2;
hence A ` <> {} by XBOOLE_0:def 5; :: thesis: verum