theorem :: PCOMPS_1:28

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