let A, B, C be Point of (TOP-REAL 2); ( 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
; |((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; verum