METRIC SPACE
Definition
An object is a <METRIC SPACE> if and only if: it is a <STRUCTURE(math)> with principal set S; it contains an <ORDERED SET> and <ALGEBRAIC GROUP> (D, +D, 0D); it contains a <METRIC FUNCTION> f from pairs of members of S to D