let A, B, C be Point of (TOP-REAL 2); ( A,B,C is_a_triangle & |((B - A),(C - A))| = 0 & not |.(C - B).| * (sin (angle (C,B,A))) = |.(A - C).| implies |.(C - B).| * (- (sin (angle (C,B,A)))) = |.(A - C).| )
assume that
A1:
A,B,C is_a_triangle
and
A2:
|((B - A),(C - A))| = 0
; ( |.(C - B).| * (sin (angle (C,B,A))) = |.(A - C).| or |.(C - B).| * (- (sin (angle (C,B,A)))) = |.(A - C).| )
A3:
A,B,C are_mutually_distinct
by A1, EUCLID_6:20;
then A4:
|.(C - B).| * (sin (angle (C,B,A))) = |.(C - A).| * (sin (angle (B,A,C)))
by EUCLID_6:6;
( sin (angle (B,A,C)) = 1 or sin (angle (B,A,C)) = - 1 )
by A2, A3, SIN_COS:77, EUCLID_3:45;
hence
( |.(C - B).| * (sin (angle (C,B,A))) = |.(A - C).| or |.(C - B).| * (- (sin (angle (C,B,A)))) = |.(A - C).| )
by A4, EUCLID_6:43; verum