:: deftheorem defines median EUCLID12:def 7 :
for A, B, C being Point of (TOP-REAL 2) holds median (A,B,C) = Line (A,(the_midpoint_of_the_segment (B,C)));