theorem Th45: :: EUCLID13:55

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