theorem Th38ThJ8: :: EUCLID13:47

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