[mizar] Att: John Harrison

[trybulec <trybulec@math.uwb.edu.pl>]

Dera John,

let me cite your article:
  'We normally write "(x+y)/(x-y) rather than "the product of, on the 
one hand the sum of the first unknown ..."'

You might be interested in a contemporary effort to be informal:

It is from "Webster's New Collegiate Dictionary" - entry for 'metric' 
(third meaning)

'a mathematical function that associates with each pair of elements of a 
set a real nonnegative number constituting their distance and satisfying 
the conditions that the number is zero if the two elements are 
identical, the number is the same regardless of the order in which the 
two elements are taken, and the number associated with one pair of 
elements plus that associated with one member of the pair and third 
element is equal to or greater than the number associated with the other 
member of the pair and the third element'

Looks correct. But the triangle inequality is stronger than usual.

Regards,
Andrzej