let n be Element of NAT ; :: thesis: for A being Subset of (TOP-REAL n) st A is Bounded holds
Cl A is Bounded
let A be Subset of (TOP-REAL n); :: thesis: ( A is Bounded implies Cl A is Bounded )
assume A is bounded Subset of (Euclid n) ; :: according to JORDAN2C:def 2 :: thesis: Cl A is Bounded
then consider r being Real, x being Point of (Euclid n) such that
0 < r and
A1: A c= Ball x,r by METRIC_6:def 10;
A2: Ball x,r c= cl_Ball x,r by METRIC_1:15;
reconsider D = Cl A as Subset of (Euclid n) by TOPREAL3:13;
reconsider B = cl_Ball x,r as Subset of (TOP-REAL n) by TOPREAL3:13;
X: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider E = B as Subset of (TopSpaceMetr (Euclid n)) ;
E is closed by Th65;
then A3: B is closed by X, PRE_TOPC:61;
A c= B by A1, A2, XBOOLE_1:1;
then Cl A c= Cl B by PRE_TOPC:49;
then Cl A c= B by A3, PRE_TOPC:52;
then D is bounded by Th67, TBSP_1:21;
hence Cl A is Bounded by JORDAN2C:def 2; :: thesis: verum