let n be Nat; :: thesis: for A being Subset of (TOP-REAL n) st A is compact holds
A is bounded
let A be Subset of (TOP-REAL n); :: thesis: ( A is compact implies A is bounded )
assume A1: A is compact ; :: thesis: A is bounded
A c= the carrier of ((TOP-REAL n) | A) by PRE_TOPC:8;
then reconsider A2 = A as Subset of ((TOP-REAL n) | A) ;

per cases ( A <> {} or A = {} ) ;

suppose A <> {} ; :: thesis: A is bounded

then reconsider A1 = A as non empty Subset of (Euclid n) by TOPREAL3:8;
[#] ((TOP-REAL n) | A) = A2 by PRE_TOPC:def 5;
then [#] ((TOP-REAL n) | A) is compact by A1, COMPTS_1:2;
then A2: (TOP-REAL n) | A is compact by COMPTS_1:1;
TopSpaceMetr ((Euclid n) | A1) = (TOP-REAL n) | A by EUCLID:63;
then (Euclid n) | A1 is totally_bounded by A2, TBSP_1:9;
then A3: (Euclid n) | A1 is bounded by TBSP_1:19;
[#] ((Euclid n) | A1) = A1 by TOPMETR:def 2;
then A1 is bounded by A3, Th49;
hence A is bounded by Th5; :: thesis: verum

end;

suppose A = {} ; :: thesis: A is bounded

hence A is bounded ; :: thesis: verum

end;

end;