theorem Thm21: :: EUCLID10:34

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle & angle (B,A,C) = PI / 2 holds
( |.(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).| )