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 )
reconsider D = Cl A as Subset of (Euclid n) by TOPREAL3:8;
assume A is bounded Subset of (Euclid n) ; :: according to JORDAN2C:def 1 :: 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 3;
reconsider B = cl_Ball (x,r) as Subset of (TOP-REAL n) by TOPREAL3:8;
Ball (x,r) c= cl_Ball (x,r) by METRIC_1:14;
then A c= B by A1, XBOOLE_1:1;
then A2: Cl A c= Cl B by PRE_TOPC:19;
A3: 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 B is closed by A3, PRE_TOPC:31;
then Cl A c= B by A2, PRE_TOPC:22;
then D is bounded by Th67, TBSP_1:14;
hence Cl A is Bounded by JORDAN2C:def 1; :: thesis: verum