theorem Th41: :: EUCLID13:50

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