theorem Th48: :: EUCLID13:59

for r being Real
for A, B, C, D being Point of (TOP-REAL 2) st B <> C & r = - ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) & D = (r * B) + ((1 - r) * C) & D <> C holds
D = the_foot_of_the_altitude (A,B,C)