:: deftheorem defines is_between METRIC_1:def 22 :
for S being MetrStruct
for p, q, r being Element of S holds
( q is_between p,r iff ( p <> q & p <> r & q <> r & dist (p,r) = (dist (p,q)) + (dist (q,r)) ) );