for A, B being Point of (TOP-REAL 2) holds half_length (A,B) = half_length (B,A) by EUCLID_6:43;