for n being Nat
for p, q being Point of (TOP-REAL n) holds |(p,q)| <= |(p,p)| + |(q,q)|