let Nrm be RealNormSpace; :: thesis: for X being Subset of Nrm st X is compact holds
( X is closed & ex r being Real st
for y being Point of Nrm st y in X holds
||.y.|| < r )
let X be Subset of Nrm; :: thesis: ( X is compact implies ( X is closed & ex r being Real st
for y being Point of Nrm st y in X holds
||.y.|| < r ) )
assume A1: X is compact ; :: thesis: ( X is closed & ex r being Real st
for y being Point of Nrm st y in X holds
||.y.|| < r )

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

suppose A2: X = {} ; :: thesis: ( X is closed & ex r being Real st
for y being Point of Nrm st y in X holds
||.y.|| < r )

reconsider Y = X as Subset of (TopSpaceNorm Nrm) ;
Y is closed by A2;
hence X is closed by NORMSP_2:15; :: thesis: ex r being Real st
for y being Point of Nrm st y in X holds
||.y.|| < r
thus ex r being Real st
for y being Point of Nrm st y in X holds
||.y.|| < r :: thesis: verum

proof

take 1 ; :: thesis: for y being Point of Nrm st y in X holds
||.y.|| < 1
thus for y being Point of Nrm st y in X holds
||.y.|| < 1 by A2; :: thesis: verum

end;

end;

suppose A3: X <> {} ; :: thesis: ( X is closed & ex r being Real st
for y being Point of Nrm st y in X holds
||.y.|| < r )

thus X is closed :: thesis: ex r being Real st
for y being Point of Nrm st y in X holds
||.y.|| < r

proof

assume not X is closed ; :: thesis: contradiction
then consider s1 being sequence of Nrm such that
A4: rng s1 c= X and
A5: ( s1 is convergent & not lim s1 in X ) ;
ex s2 being sequence of Nrm st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) by A1, A4;
hence contradiction by A5, LOPBAN_3:8; :: thesis: verum

end;

reconsider Y = X as Subset of (MetricSpaceNorm Nrm) ;
A6: Y is sequentially_compact by A1, TOPMETR4:18;
reconsider Z = Y as Subset of (TopSpaceMetr (MetricSpaceNorm Nrm)) ;
Z is compact by TOPMETR4:15, A6;
then consider r0 being Real such that
A7: ( 0 < r0 & ( for x, y being Point of (MetricSpaceNorm Nrm) st x in Y & y in Y holds
dist (x,y) <= r0 ) ) by HAUSDORF:18, TBSP_1:def 7;
consider x0 being object such that
A8: x0 in Y by A3, XBOOLE_0:def 1;
reconsider x0 = x0 as Point of (MetricSpaceNorm Nrm) by A8;
reconsider x = x0 as Point of Nrm ;
set r = (1 + r0) + ||.x.||;
reconsider r = (1 + r0) + ||.x.|| as Real ;
take r ; :: thesis: for y being Point of Nrm st y in X holds
||.y.|| < r
thus for y being Point of Nrm st y in X holds
||.y.|| < r :: thesis: verum

proof

let y be Point of Nrm; :: thesis: ( y in X implies ||.y.|| < r )
assume A9: y in X ; :: thesis: ||.y.|| < r
reconsider y0 = y as Point of (MetricSpaceNorm Nrm) ;
y = x + (y - x) by RLVECT_4:1;
then A10: ||.y.|| <= ||.x.|| + ||.(y - x).|| by NORMSP_1:def 1;
||.(y - x).|| = dist (y0,x0) by NORMSP_2:def 1;
then ||.(y - x).|| + 0 < r0 + 1 by A7, A8, A9, XREAL_1:8;
then ||.x.|| + ||.(y - x).|| < ||.x.|| + (r0 + 1) by XREAL_1:8;
hence ||.y.|| < r by A10, XXREAL_0:2; :: thesis: verum

end;

end;

end;