let M be non empty MetrSpace; :: thesis: for z being Point of M
for r being Real holds Sphere (z,r) is bounded
let z be Point of M; :: thesis: for r being Real holds Sphere (z,r) is bounded
let r be Real; :: thesis: Sphere (z,r) is bounded
Sphere (z,r) c= cl_Ball (z,r) by METRIC_1:15;
hence Sphere (z,r) is bounded by Th57, TBSP_1:14; :: thesis: verum