theorem Th65: :: EUCLID13:77

for A, B, C being Point of (TOP-REAL 2) st A,C,B is_a_triangle & angle (C,A,B) = PI / 2 holds
the_length_of_the_altitude (C,A,B) = |.(A - B).| * (tan (angle (A,B,C)))