theorem :: EUCLID12:84

for A, B being Point of (TOP-REAL 2) holds median (B,A,A) = Line (A,B) by Th24;