:: deftheorem defines the_centroid_of_the_triangle EUCLID12:def 8 :
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
for b₄ being Point of (TOP-REAL 2) holds
( b₄ = the_centroid_of_the_triangle (A,B,C) iff ( (median (A,B,C)) /\ (median (B,C,A)) = {b₄} & (median (B,C,A)) /\ (median (C,A,B)) = {b₄} & (median (C,A,B)) /\ (median (A,B,C)) = {b₄} ) );