let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & angle (B,A,C) = PI / 2 implies ( |.(C - B).| * (sin (angle (C,B,A))) = |.(A - C).| & |.(C - B).| * (sin (angle (A,C,B))) = |.(A - B).| & |.(C - B).| * (cos (angle (C,B,A))) = |.(A - B).| & |.(C - B).| * (cos (angle (A,C,B))) = |.(A - C).| ) )
assume that
A1: A,B,C is_a_triangle and
A2: angle (B,A,C) = PI / 2 ; :: thesis: ( |.(C - B).| * (sin (angle (C,B,A))) = |.(A - C).| & |.(C - B).| * (sin (angle (A,C,B))) = |.(A - B).| & |.(C - B).| * (cos (angle (C,B,A))) = |.(A - B).| & |.(C - B).| * (cos (angle (A,C,B))) = |.(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;
A5: |.(B - A).| * (sin (angle (B,A,C))) = |.(B - C).| * (sin (angle (A,C,B))) by A3, EUCLID_6:6;
thus A6: |.(C - B).| * (sin (angle (C,B,A))) = |.(A - C).| by A2, A4, SIN_COS:77, EUCLID_6:43; :: thesis: ( |.(C - B).| * (sin (angle (A,C,B))) = |.(A - B).| & |.(C - B).| * (cos (angle (C,B,A))) = |.(A - B).| & |.(C - B).| * (cos (angle (A,C,B))) = |.(A - C).| )
|.(A - B).| * (sin (angle (B,A,C))) = |.(B - C).| * (sin (angle (A,C,B))) by A5, EUCLID_6:43;
hence A7: |.(C - B).| * (sin (angle (A,C,B))) = |.(A - B).| by A2, SIN_COS:77, EUCLID_6:43; :: thesis: ( |.(C - B).| * (cos (angle (C,B,A))) = |.(A - B).| & |.(C - B).| * (cos (angle (A,C,B))) = |.(A - C).| )
((angle (B,A,C)) + (angle (A,C,B))) + (angle (C,B,A)) = PI by A2, A3, COMPTRIG:5, EUCLID_3:47;
then sin (angle (A,C,B)) = sin ((PI / 2) - (angle (C,B,A))) by A2;
hence |.(C - B).| * (cos (angle (C,B,A))) = |.(A - B).| by A7, SIN_COS:79; :: thesis: |.(C - B).| * (cos (angle (A,C,B))) = |.(A - C).|
((angle (B,A,C)) + (angle (A,C,B))) + (angle (C,B,A)) = PI by A2, A3, COMPTRIG:5, EUCLID_3:47;
then sin (angle (C,B,A)) = sin ((PI / 2) - (angle (A,C,B))) by A2;
hence |.(C - B).| * (cos (angle (A,C,B))) = |.(A - C).| by A6, SIN_COS:79; :: thesis: verum