theorem :: EUCLID10:52

for A, B, C, P being Point of (TOP-REAL 2) st 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 holds
|.(A - P).| * (sin (PI - (((angle (C,B,A)) / 3) + ((angle (B,A,C)) / 3)))) = |.(A - B).| * (sin ((angle (C,B,A)) / 3))