let A be Point of (TOP-REAL 2); :: thesis: half_length (A,A) = 0
half_length (A,A) = (1 / 2) * 0 by EUCLID_6:42;
hence half_length (A,A) = 0 ; :: thesis: verum