theorem :: EUCLID13:79

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