for T being non empty Reflexive symmetric triangle MetrStruct
for t1 being Element of T
for r being Real st 0 < r holds
diameter (Ball (t1,r)) <= 2 * r