theorem Th47: :: EUCLID13:58

for A, B, C being Point of (TOP-REAL 2) st B <> C & |((B - A),(B - C))| = 0 holds
|.((the_foot_of_the_altitude (A,B,C)) - A).| = |.(A - B).|