theorem Th62: :: EUCLID12:86

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
ex D being Point of (TOP-REAL 2) st
( D in median (A,B,C) & D in median (B,C,A) & D in median (C,A,B) )