let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,C,B is_a_triangle & |((A - C),(A - B))| = 0 implies the_length_of_the_altitude (C,A,B) = |.(A - B).| * |.(tan (angle (A,B,C))).| )
assume that
A1: A,C,B is_a_triangle and
A2: |((A - C),(A - B))| = 0 ; :: thesis: the_length_of_the_altitude (C,A,B) = |.(A - B).| * |.(tan (angle (A,B,C))).|
A3: ( A,C,B are_mutually_distinct & |((C - A),(B - A))| = 0 ) by A2, Th10, A1, EUCLID_6:20;
A4: |.(A - B).| <> 0 by A3, EUCLID_6:42;

per cases ( angle (C,A,B) = PI / 2 or angle (C,A,B) = (3 / 2) * PI ) by A3, EUCLID_3:45;

suppose angle (C,A,B) = PI / 2 ; :: thesis: the_length_of_the_altitude (C,A,B) = |.(A - B).| * |.(tan (angle (A,B,C))).|

then A5: the_length_of_the_altitude (C,A,B) = |.(A - B).| * (tan (angle (A,B,C))) by A1, Th65;
then 0 <= tan (angle (A,B,C)) by A4, A3, Th46;
hence the_length_of_the_altitude (C,A,B) = |.(A - B).| * |.(tan (angle (A,B,C))).| by A5, ABSVALUE:def 1; :: thesis: verum

end;

suppose A6: angle (C,A,B) = (3 / 2) * PI ; :: thesis: the_length_of_the_altitude (C,A,B) = |.(A - B).| * |.(tan (angle (A,B,C))).|

A7: A,B,C is_a_triangle by A1, MENELAUS:15;
tan (angle (C,B,A)) = tan ((2 * PI) - (angle (A,B,C))) by A1, EUCLID10:31
.= - (tan (angle (A,B,C))) by Th6 ;
then A8: (- (tan (angle (A,B,C)))) * |.(A - B).| = the_length_of_the_altitude (C,A,B) by A7, A6, Th66;
then tan (angle (A,B,C)) <= 0 by A4, A3, Th46;
hence the_length_of_the_altitude (C,A,B) = |.(A - B).| * |.(tan (angle (A,B,C))).| by A8, ABSVALUE:30; :: thesis: verum

end;

end;