theorem :: EUCLID13:46

for A, B, C being Point of (TOP-REAL 2) st B <> C & the_foot_of_the_altitude (A,B,C) = A holds
A in Line (B,C) by Th35;