theorem Th39: :: EUCLID13:48

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