let p be Point of (Euclid 2); :: thesis: for r being Real
for B being Subset of (TOP-REAL 2) st B = cl_Ball p,r holds
B is compact
let r be Real; :: thesis: for B being Subset of (TOP-REAL 2) st B = cl_Ball p,r holds
B is compact
let B be Subset of (TOP-REAL 2); :: 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