let n be Nat; :: thesis: for A being Subset of (TOP-REAL n)
for a being bounded Subset of (Euclid n) st a = A holds
for p being Point of (Euclid n) st p in conv A holds
conv A c= cl_Ball (p,(diameter a))
let A be Subset of (TOP-REAL n); :: thesis: for a being bounded Subset of (Euclid n) st a = A holds
for p being Point of (Euclid n) st p in conv A holds
conv A c= cl_Ball (p,(diameter a))
A1: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
let a be bounded Subset of (Euclid n); :: thesis: ( a = A implies for p being Point of (Euclid n) st p in conv A holds
conv A c= cl_Ball (p,(diameter a)) )
assume A2: A = a ; :: thesis: for p being Point of (Euclid n) st p in conv A holds
conv A c= cl_Ball (p,(diameter a))
let x be Point of (Euclid n); :: thesis: ( x in conv A implies conv A c= cl_Ball (x,(diameter a)) )
assume A3: x in conv A ; :: thesis: conv A c= cl_Ball (x,(diameter a))
A4: A c= cl_Ball (x,(diameter a))

proof

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in A or p in cl_Ball (x,(diameter a)) )
assume A5: p in A ; :: thesis: p in cl_Ball (x,(diameter a))
then reconsider p = p as Point of (Euclid n) by A2;
reconsider pp = p as Point of (TOP-REAL n) by A1;
A6: cl_Ball (p,(diameter a)) = cl_Ball (pp,(diameter a)) by TOPREAL9:14;
A c= cl_Ball (p,(diameter a))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in A or y in cl_Ball (p,(diameter a)) )
assume A7: y in A ; :: thesis: y in cl_Ball (p,(diameter a))
then reconsider q = y as Point of (Euclid n) by A2;
dist (p,q) <= diameter a by A2, A5, A7, TBSP_1:def 8;
hence y in cl_Ball (p,(diameter a)) by METRIC_1:12; :: thesis: verum

end;

then conv A c= cl_Ball (pp,(diameter a)) by A6, CONVEX1:30;
then dist (p,x) <= diameter a by A3, A6, METRIC_1:12;
hence p in cl_Ball (x,(diameter a)) by METRIC_1:12; :: thesis: verum

end;

reconsider xx = x as Point of (TOP-REAL n) by A1;
cl_Ball (x,(diameter a)) = cl_Ball (xx,(diameter a)) by TOPREAL9:14;
hence conv A c= cl_Ball (x,(diameter a)) by A4, CONVEX1:30; :: thesis: verum