theorem :: EUCLID12:24

for A being Point of (TOP-REAL 2) holds half_length (A,A) = 0