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;

per cases then ( |.((the_foot_of_the_altitude (C,A,B)) - C).| = |.(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)))))) or |.((the_foot_of_the_altitude (C,A,B)) - C).| = |.(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))))))) ) by A4;

suppose A7: |.((the_foot_of_the_altitude (C,A,B)) - C).| = |.(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)))))) ; :: 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)))))).|

|.(A - B).| <> 0 by A5, EUCLID_6:42;
then A8: 0 <= ((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))))) by A7;
the_length_of_the_altitude (C,A,B) = |.(C - (the_foot_of_the_altitude (C,A,B))).| by A5, Def3
.= |.((the_foot_of_the_altitude (C,A,B)) - C).| by EUCLID_6:43
.= |.(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)))))).| by A7, A8, ABSVALUE:def 1 ;
hence 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)))))).| ; :: thesis: verum

end;

suppose A10: |.((the_foot_of_the_altitude (C,A,B)) - C).| = |.(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))))))) ; :: 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)))))).|

|.(A - B).| <> 0 by A5, EUCLID_6:42;
then A11: ((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))))) <= 0 by A10;
the_length_of_the_altitude (C,A,B) = |.(C - (the_foot_of_the_altitude (C,A,B))).| by A5, Def3
.= |.((the_foot_of_the_altitude (C,A,B)) - C).| by EUCLID_6:43
.= |.(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)))))).| by A10, A11, ABSVALUE:30 ;
hence 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)))))).| ; :: thesis: verum

end;

end;