:: deftheorem defines close_dist_Segment METRIC_1:def 24 :
for M being non empty MetrStruct
for p, r being Element of M holds close_dist_Segment (p,r) = { q where q is Element of M : q is_between p,r } \/ {p,r};