:: deftheorem defines convex VECTMETR:def 1 :
for V being non empty MetrStruct holds
( V is convex iff for x, y being Element of V
for r being Real st 0 <= r & r <= 1 holds
ex z being Element of V st
( dist (x,z) = r * (dist (x,y)) & dist (z,y) = (1 - r) * (dist (x,y)) ) );