let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,C,B is_a_triangle & angle (A,C,B) < PI & |((A - C),(A - B))| <> 0 implies the_length_of_the_altitude (C,A,B) = |.(A - B).| * |.(((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))).| )
assume that
A1: A,C,B is_a_triangle and
A2: angle (A,C,B) < PI and
A3: |((A - C),(A - B))| <> 0 ; :: thesis: the_length_of_the_altitude (C,A,B) = |.(A - B).| * |.(((sin (angle (C,B,A))) / (sin ((angle (B,A,C)) + (angle (C,B,A))))) * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))).|
A4: |.(A - C).| = (|.(A - B).| * (sin (angle (C,B,A)))) / (sin ((angle (B,A,C)) + (angle (C,B,A)))) by A1, A2, Th64;
A5: ( C,A,B is_a_triangle & A,C,B are_mutually_distinct ) by A1, EUCLID_6:20, MENELAUS:15;
then ( |.((the_foot_of_the_altitude (C,A,B)) - C).| = |.(C - A).| * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B))))) or |.((the_foot_of_the_altitude (C,A,B)) - C).| = |.(C - A).| * (- (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))) ) by A3, Th45, Th67;
then ( |.((the_foot_of_the_altitude (C,A,B)) - C).| = |.(A - C).| * (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B))))) or |.((the_foot_of_the_altitude (C,A,B)) - C).| = |.(A - C).| * (- (sin (angle (C,A,(the_foot_of_the_altitude (C,A,B)))))) ) by EUCLID_6:43;