:: 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_{4} being Point of (TOP-REAL 2) holds

( b_{4} = the_centroid_of_the_triangle (A,B,C) iff ( (median (A,B,C)) /\ (median (B,C,A)) = {b_{4}} & (median (B,C,A)) /\ (median (C,A,B)) = {b_{4}} & (median (C,A,B)) /\ (median (A,B,C)) = {b_{4}} ) );

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds

for b

( b