theorem Th7: :: EUCLID11:12

for A, B, C, F being Point of (TOP-REAL 2) st A,F,C is_a_triangle & angle (C,F,A) < PI & angle (A,C,F) = (angle (A,C,B)) / 3 & angle (F,A,C) = (angle (B,A,C)) / 3 & (((angle (A,C,B)) / 3) + ((angle (B,A,C)) / 3)) + ((angle (C,B,A)) / 3) = PI / 3 holds
|.(A - F).| * (sin ((PI / 3) - ((angle (C,B,A)) / 3))) = |.(A - C).| * (sin ((angle (A,C,B)) / 3))