:: deftheorem defines is_Between GTARSKI1:def 14 :
for S being MetrStruct
for p, q, r being Element of S holds
( q is_Between p,r iff dist (p,r) = (dist (p,q)) + (dist (q,r)) );