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