consider L1, L2 being Element of line_of_REAL 2 such that
A2:
the_altitude (A,B,C) = L1
and
A3:
L2 = Line (B,C)
and
A in L1
and
A4:
L1 _|_ L2
by A1, Def1;
consider x being Element of REAL 2 such that
A5:
L1 /\ L2 = {x}
by A4, EUCLID12:43;
reconsider P = x as Point of (TOP-REAL 2) by EUCLID:22;
take
P
; ex P being Point of (TOP-REAL 2) st
( P = P & (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} )
thus
ex P being Point of (TOP-REAL 2) st
( P = P & (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} )
by A2, A3, A5; verum