for M being non empty MetrSpace
for u being Point of M
for P being Subset of (TopSpaceMetr M) holds
( u in Int P iff ex r being Real st
( r > 0 & Ball (u,r) c= P ) )