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