let A, B, C be Point of (TOP-REAL 2); :: thesis: ( 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 ; :: thesis: ( |.(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; :: thesis: verum