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: n in NAT by ORDINAL1:def 12;
A2: 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 A3: 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 A4: x in conv A ; :: thesis: conv A c= cl_Ball (x,(diameter a))
A5: A c= cl_Ball (x,(diameter a))

proof

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in A or y in cl_Ball (p,(diameter a)) )
assume A8: y in A ; :: thesis: y in cl_Ball (p,(diameter a))
then reconsider q = y as Point of (Euclid n) by A3;
dist (p,q) <= diameter a by A3, A6, A8, 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 A7, CONVEX1:30;
then dist (p,x) <= diameter a by A4, A7, 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 A2;
cl_Ball (x,(diameter a)) = cl_Ball (xx,(diameter a)) by A1, TOPREAL9:14;
hence conv A c= cl_Ball (x,(diameter a)) by A5, CONVEX1:30; :: thesis: verum