let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & |((B - A),(B - C))| <> 0 & 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: A,B,C is_a_triangle and
A2: |((B - A),(B - C))| <> 0 ; :: 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).| )
A,B,C are_mutually_distinct by A1, EUCLID_6:20;
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 A1, A2, Th67, Th45; :: thesis: verum