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 Th14;
hence B is compact by TOPREAL6:79; :: thesis: verum