theorem Th15: :: TOPMETR:15

for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M) holds
( P is open iff for p being Point of M st p in P holds
ex r being Real st
( r > 0 & Ball (p,r) c= P ) ) by PCOMPS_1:def 4;