:: deftheorem Def19 defines ultra METRIC_1:def 19 :
for M being non empty MetrStruct holds
( M is ultra iff for a, b, c being Element of M holds dist (a,c) <= max ((dist (a,b)),(dist (b,c))) );