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 ; :: thesis: 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; :: thesis: verum