for p1, p2 being Point of (TOP-REAL 2) holds |.(p1 - p2).| = |.(p2 - p1).| by Lm2;