theorem :: EUCLID10:32

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & |((B - A),(C - A))| = 0 & not |.(C - B).| * (sin (angle (C,B,A))) = |.(A - C).| holds
|.(C - B).| * (- (sin (angle (C,B,A)))) = |.(A - C).|