let p be Point of ; :: thesis: for r being Real
for B being Subset of st B = cl_Ball p,r holds
B is compact
let r be Real; :: thesis: for B being Subset of st B = cl_Ball p,r holds
B is compact
let B be Subset of ; :: thesis: ( B = cl_Ball p,r implies B is compact )
assume B = cl_Ball p,r ; :: thesis: B is compact
then ( B is Bounded & B is closed ) by Th21;
hence B is compact by TOPREAL6:88; :: thesis: verum