theorem Thm35:
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 &
(((angle (C,B,A)) / 3) + ((angle (B,A,C)) / 3)) + ((angle (A,C,B)) / 3) = PI / 3 holds
|.(A - P).| * (sin (((2 * PI) / 3) + ((angle (A,C,B)) / 3))) = |.(A - B).| * (sin ((angle (C,B,A)) / 3))