:: deftheorem Def1 defines Balls FRECHET:def 1 :
for M being non empty MetrStruct
for x being Point of (TopSpaceMetr M)
for b₃ being Subset-Family of (TopSpaceMetr M) holds
( b₃ = Balls x iff ex y being Point of M st
( y = x & b₃ = { (Ball (y,(1 / n))) where n is Nat : n <> 0 } ) );