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