let n be Element of NAT ; :: thesis: for p being Point of (Euclid n)
for r being Real
for B being Subset of (TOP-REAL n) st B = cl_Ball p,r holds
( B is Bounded & B is closed )
let p be Point of (Euclid n); :: thesis: for r being Real
for B being Subset of (TOP-REAL n) st B = cl_Ball p,r holds
( B is Bounded & B is closed )
let r be Real; :: thesis: for B being Subset of (TOP-REAL n) st B = cl_Ball p,r holds
( B is Bounded & B is closed )
let B be Subset of (TOP-REAL n); :: thesis: ( B = cl_Ball p,r implies ( B is Bounded & B is closed ) )
assume A1: B = cl_Ball p,r ; :: thesis: ( B is Bounded & B is closed )
XX: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider BB = B as Subset of (TopSpaceMetr (Euclid n)) by A1;
cl_Ball p,r c= Ball p,(r + 1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in cl_Ball p,r or x in Ball p,(r + 1) )
assume A2: x in cl_Ball p,r ; :: thesis: x in Ball p,(r + 1)
then reconsider q = x as Point of (Euclid n) ;
A3: dist p,q <= r by A2, METRIC_1:13;
r < r + 1 by XREAL_1:31;
then dist p,q < r + 1 by A3, XXREAL_0:2;
hence x in Ball p,(r + 1) by METRIC_1:12; :: thesis: verum

end;

then cl_Ball p,r is bounded by TBSP_1:19, TBSP_1:21;
hence B is Bounded by A1, JORDAN2C:def 2; :: thesis: B is closed
BB is closed by A1, TOPREAL6:65;
hence B is closed by XX, PRE_TOPC:61, A1; :: thesis: verum