let A, B, C be Point of (TOP-REAL 2); :: thesis: ( B <> C & the_foot_of_the_altitude (A,B,C),B,A is_a_triangle & not |.(A - B).| * (sin (angle (A,B,(the_foot_of_the_altitude (A,B,C))))) = |.((the_foot_of_the_altitude (A,B,C)) - A).| implies |.(A - B).| * (- (sin (angle (A,B,(the_foot_of_the_altitude (A,B,C)))))) = |.((the_foot_of_the_altitude (A,B,C)) - A).| )
assume that
A1: B <> C and
A2: the_foot_of_the_altitude (A,B,C),B,A is_a_triangle ; :: thesis: ( |.(A - B).| * (sin (angle (A,B,(the_foot_of_the_altitude (A,B,C))))) = |.((the_foot_of_the_altitude (A,B,C)) - A).| or |.(A - B).| * (- (sin (angle (A,B,(the_foot_of_the_altitude (A,B,C)))))) = |.((the_foot_of_the_altitude (A,B,C)) - A).| )
|((B - (the_foot_of_the_altitude (A,B,C))),(A - (the_foot_of_the_altitude (A,B,C))))| = 0 by A1, Th39;
hence ( |.(A - B).| * (sin (angle (A,B,(the_foot_of_the_altitude (A,B,C))))) = |.((the_foot_of_the_altitude (A,B,C)) - A).| or |.(A - B).| * (- (sin (angle (A,B,(the_foot_of_the_altitude (A,B,C)))))) = |.((the_foot_of_the_altitude (A,B,C)) - A).| ) by A2, EUCLID10:32; :: thesis: verum