theorem :: FINTOPO8:62

for x being Point of FMT_R^1
for z being Point of (TopSpaceMetr RealSpace) st x = z holds
Balls z is Subset-Family of FMT_R^1 by FINTOPO7:def 15, TOPMETR:def 6;