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