let A, B, C be Point of (TOP-REAL 2); ( B <> C & |((B - A),(B - C))| = 0 implies |.((the_foot_of_the_altitude (A,B,C)) - A).| = |.(A - B).| )
assume that
A1:
B <> C
and
A2:
|((B - A),(B - C))| = 0
; |.((the_foot_of_the_altitude (A,B,C)) - A).| = |.(A - B).|
|.((the_foot_of_the_altitude (A,B,C)) - A).| = |.(B - A).|
by A1, A2, Th43;
hence
|.((the_foot_of_the_altitude (A,B,C)) - A).| = |.(A - B).|
by EUCLID_6:43; verum