let A, B, C be Point of (TOP-REAL 2); :: thesis: ( B <> C implies the_length_of_the_altitude (A,B,C) = the_length_of_the_altitude (A,C,B) )
assume A1: B <> C ; :: thesis: the_length_of_the_altitude (A,B,C) = the_length_of_the_altitude (A,C,B)
then the_length_of_the_altitude (A,B,C) = |.(A - (the_foot_of_the_altitude (A,B,C))).| by Def3
.= |.(A - (the_foot_of_the_altitude (A,C,B))).| by A1, Th34
.= the_length_of_the_altitude (A,C,B) by A1, Def3 ;
hence the_length_of_the_altitude (A,B,C) = the_length_of_the_altitude (A,C,B) ; :: thesis: verum