let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies A <> the_foot_of_the_altitude (A,B,C) )
assume A1: A,B,C is_a_triangle ; :: thesis: A <> the_foot_of_the_altitude (A,B,C)
assume A2: A = the_foot_of_the_altitude (A,B,C) ; :: thesis: contradiction
A3: A,B,C are_mutually_distinct by A1, EUCLID_6:20;
then A in Line (B,C) by A2, Th35;
hence contradiction by A1, A3, MENELAUS:13; :: thesis: verum