let A, B, C be Point of (TOP-REAL 2); ( B <> C & A in Line (B,C) implies the_foot_of_the_altitude (A,B,C) = A )
assume that
A1:
B <> C
and
A2:
A in Line (B,C)
; the_foot_of_the_altitude (A,B,C) = A
consider P being Point of (TOP-REAL 2) such that
A3:
the_foot_of_the_altitude (A,B,C) = P
and
A4:
(the_altitude (A,B,C)) /\ (Line (B,C)) = {P}
by A1, Def2;
consider L1, L2 being Element of line_of_REAL 2 such that
A5:
the_altitude (A,B,C) = L1
and
A6:
L2 = Line (B,C)
and
A7:
A in L1
and
L1 _|_ L2
by A1, Def1;
A in L1 /\ L2
by A6, A7, A2, XBOOLE_0:def 4;
hence
the_foot_of_the_altitude (A,B,C) = A
by A3, A4, A5, A6, TARSKI:def 1; verum