let A, B, C, F be Point of (TOP-REAL 2); :: thesis: ( 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 implies |.(A - F).| * (sin ((PI / 3) - ((angle (C,B,A)) / 3))) = |.(A - C).| * (sin ((angle (A,C,B)) / 3)) )
assume that
A1: A,F,C is_a_triangle and
A2: angle (C,F,A) < PI and
A3: angle (A,C,F) = (angle (A,C,B)) / 3 and
A4: angle (F,A,C) = (angle (B,A,C)) / 3 and
A5: (((angle (A,C,B)) / 3) + ((angle (B,A,C)) / 3)) + ((angle (C,B,A)) / 3) = PI / 3 ; :: thesis: |.(A - F).| * (sin ((PI / 3) - ((angle (C,B,A)) / 3))) = |.(A - C).| * (sin ((angle (A,C,B)) / 3))
A6: angle (F,C,A) = (2 * PI) - ((angle (A,C,B)) / 3) by A1, A3, EUCLID10:31;
A7: ( angle (A,C,F) = (2 * PI) - (angle (F,C,A)) & angle (F,A,C) = (2 * PI) - (angle (C,A,F)) ) by A1, EUCLID10:31;
A8: A,F,C are_mutually_distinct by A1, EUCLID_6:20;
( F,A,C is_a_triangle & angle (C,F,A) < PI ) by A1, A2, MENELAUS:15;
then ((angle (C,A,F)) + (angle (A,F,C))) + (angle (F,C,A)) = 5 * PI by EUCLID10:54;
then angle (A,F,C) = ((4 * PI) / 3) - ((angle (C,B,A)) / 3) by A7, A3, A5, A4;
then A9: sin (angle (A,F,C)) = - (sin ((PI / 3) - ((angle (C,B,A)) / 3))) by Lm5;
|.(A - F).| * (sin (angle (A,F,C))) = |.(A - C).| * (sin ((2 * PI) - ((angle (A,C,B)) / 3))) by A8, A6, EUCLID_6:6;
then |.(A - F).| * (- (sin ((PI / 3) - ((angle (C,B,A)) / 3)))) = |.(A - C).| * (- (sin ((angle (A,C,B)) / 3))) by A9, EUCLID10:3;
hence |.(A - F).| * (sin ((PI / 3) - ((angle (C,B,A)) / 3))) = |.(A - C).| * (sin ((angle (A,C,B)) / 3)) ; :: thesis: verum