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