theorem :: FINTOPO8:63

for x being Point of FMT_R^1
for z being Point of (TopSpaceMetr RealSpace)
for SF being Subset-Family of FMT_R^1 st x = z & SF = Balls z holds
<.SF.] = U_FMT x