theorem Th5: :: CARDFIL3:6

for M being non empty MetrSpace
for x being Point of (TopSpaceMetr M) holds Balls x is basis of (BOOL2F (NeighborhoodSystem x))