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

half_length (A,A) = (1 / 2) * 0 by EUCLID_6:42;

hence half_length (A,A) = 0 ; :: thesis: verum