for p1, p2 being Point of (TOP-REAL 2) holds p1 - p2 = |[((p1 `1) - (p2 `1)),((p1 `2) - (p2 `2))]|