let A, B, C, D be Point of (TOP-REAL 2); ( B <> C & D in Line (B,C) & D <> C implies the_foot_of_the_altitude (A,B,C) = the_foot_of_the_altitude (A,D,C) )
assume that
A1:
B <> C
and
A2:
D in Line (B,C)
and
A3:
D <> C
; the_foot_of_the_altitude (A,B,C) = the_foot_of_the_altitude (A,D,C)
consider P1 being Point of (TOP-REAL 2) such that
A4:
the_foot_of_the_altitude (A,B,C) = P1
and
A5:
(the_altitude (A,B,C)) /\ (Line (B,C)) = {P1}
by A1, Def2;
consider P2 being Point of (TOP-REAL 2) such that
A6:
the_foot_of_the_altitude (A,D,C) = P2
and
A7:
(the_altitude (A,D,C)) /\ (Line (D,C)) = {P2}
by A3, Def2;
Line (D,C) = Line (B,C)
by A2, A3, Th7;
then
{P1} = {P2}
by A7, A5, A1, A2, A3, Th33;
hence
the_foot_of_the_altitude (A,B,C) = the_foot_of_the_altitude (A,D,C)
by A4, A6, ZFMISC_1:3; verum