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

proof

assume A12: L1 // L3 ; :: thesis: contradiction
L1 <> L3

proof

assume L1 = L3 ; :: thesis: contradiction
then ( L1 _|_ L2 & L1 _|_ L4 & C in L1 & C in L2 & C in L4 ) by A6, A9, A7, A10, A2, A5, EUCLID_4:41;
then L2 = L4 by EUCLID12:16, EUCLIDLP:108;
then A in Line (B,C) by A6, A9, EUCLID_4:41;
hence contradiction by A1, A4, MENELAUS:13; :: thesis: verum

end;

hence contradiction by XBOOLE_0:3, A12, EUCLIDLP:71, A5, A8, A2, A3; :: thesis: verum

end;

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