let A, B, C, P be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & angle (C,B,A) < PI & A,B,P are_mutually_distinct & angle (P,B,A) = (angle (C,B,A)) / 3 & angle (B,A,P) = (angle (B,A,C)) / 3 & angle (A,P,B) < PI implies |.(A - P).| * (sin ((PI / 3) - ((angle (A,C,B)) / 3))) = |.(A - B).| * (sin ((angle (C,B,A)) / 3)) )
assume that
A1: A,B,C is_a_triangle and
A2: angle (C,B,A) < PI and
A3: A,B,P are_mutually_distinct and
A4: angle (P,B,A) = (angle (C,B,A)) / 3 and
A5: angle (B,A,P) = (angle (B,A,C)) / 3 and
A6: angle (A,P,B) < PI ; :: thesis: |.(A - P).| * (sin ((PI / 3) - ((angle (A,C,B)) / 3))) = |.(A - B).| * (sin ((angle (C,B,A)) / 3))
A7: (((angle (C,B,A)) / 3) + ((angle (B,A,C)) / 3)) + ((angle (A,C,B)) / 3) = PI / 3 by A1, A2, Lm12;
A8: ((angle (A,P,B)) + (angle (P,B,A))) + (angle (B,A,P)) = PI by A3, A6, EUCLID_3:47;
|.(A - P).| * (sin (PI - (((angle (C,B,A)) / 3) + ((angle (B,A,C)) / 3)))) = |.(A - B).| * (sin ((angle (C,B,A)) / 3)) by A3, A4, EUCLID_6:6, A8, A5;
hence |.(A - P).| * (sin ((PI / 3) - ((angle (A,C,B)) / 3))) = |.(A - B).| * (sin ((angle (C,B,A)) / 3)) by A7, Thm1; :: thesis: verum