let A, B, C be Point of (TOP-REAL 2); :: thesis: ( C,A,B is_a_triangle & C in the_altitude (C,A,B) & C in the_altitude (A,B,C) implies (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) is being_point )
assume that
A1: C,A,B is_a_triangle and
A2: C in the_altitude (C,A,B) and
A3: C in the_altitude (A,B,C) ; :: thesis: (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) is being_point
A4: C,A,B are_mutually_distinct by A1, EUCLID_6:20;
consider L1, L2 being Element of line_of_REAL 2 such that
A5: the_altitude (C,A,B) = L1 and
A6: L2 = Line (A,B) and
C in L1 and
A7: L1 _|_ L2 by A4, Def1;
consider L3, L4 being Element of line_of_REAL 2 such that
A8: the_altitude (A,B,C) = L3 and
A9: L4 = Line (B,C) and
A in L3 and
A10: L3 _|_ L4 by A4, Def1;
A11: not L1 // L3

proof

assume L1 // L3 ; :: thesis: contradiction
then L1 = L3 by A2, A3, A5, A8, XBOOLE_0:3, EUCLIDLP:71;
then A12: L2 // L4 by A7, A10, EUCLIDLP:111, EUCLID12:16;
( B in L2 & B in L4 ) by A6, A9, EUCLID_4:41;
then Line (A,B) = Line (B,C) by A6, A9, XBOOLE_0:3, A12, EUCLIDLP:71;
then C in Line (A,B) by EUCLID_4:41;
hence contradiction by A4, MENELAUS:13, A1; :: thesis: verum

end;

( not L1 is being_point & not L3 is being_point ) by A4, A5, A8, Th31, EUCLID12:9;
hence (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) is being_point by A5, A8, A11, EUCLID12:21; :: thesis: verum