theorem Th27: :: PCOMPS_1:27

for PM being MetrStruct
for x, y being Element of PM
for r being Real st PM is triangle & y in Ball (x,r) holds
ex p being Real st
( p > 0 & Ball (y,p) c= Ball (x,r) )