:: deftheorem defines half_length EUCLID12:def 2 :
for A, B being Point of (TOP-REAL 2) holds half_length (A,B) = (1 / 2) * |.(A - B).|;