:: deftheorem NonDist defines with_nonnegative_distance ROUGHIF2:def 14 :
for M being MetrStruct holds
( M is with_nonnegative_distance iff the distance of M is nonnegative-yielding );