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