let M be non empty MetrSpace; :: thesis: for z being Point of M
for r being real number holds Sphere z,r is bounded
let z be Point of M; :: thesis: for r being real number holds Sphere z,r is bounded
let r be real number ; :: thesis: Sphere z,r is bounded
Sphere z,r c= cl_Ball z,r by METRIC_1:16;
hence Sphere z,r is bounded by Th67, TBSP_1:21; :: thesis: verum