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

proof

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

end;

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