theorem Th40: :: EUCLID13:49

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