:: deftheorem defines being_ball-family TOPMETR:def 4 :
for M being MetrStruct
for F being Subset-Family of M holds
( F is being_ball-family iff for P being set st P in F holds
ex p being Point of M ex r being Real st P = Ball (p,r) );