theorem Th5: :: COMPL_SP:5

for r being Real
for M being non empty Reflexive symmetric triangle MetrStruct
for p being Point of M st 0 <= r holds
diameter (cl_Ball (p,r)) <= 2 * r