for q, q1, q2 being Point of (TOP-REAL 2) holds dist ((q1 + q),(q2 + q)) = dist (q1,q2)