theorem Th66: :: EUCLID13:78

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