theorem Th26: :: PCOMPS_1:26

for PM being MetrStruct
for x being Element of PM ex r being Real st
( r > 0 & Ball (x,r) c= the carrier of PM )