let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & |((C - A),(B - C))| = 0 implies ( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {C} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {C} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {C} ) )
assume that
A1: A,B,C is_a_triangle and
A2: |((C - A),(B - C))| = 0 ; :: thesis: ( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {C} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {C} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {C} )
A3: A,B,C are_mutually_distinct by A1, EUCLID_6:20;
B,C,A is_a_triangle by A1, MENELAUS:15;
then A4: ( not A in Line (B,C) & not B in Line (C,A) ) by A1, Th20;
( the_foot_of_the_altitude (A,B,C) = C & the_foot_of_the_altitude (B,C,A) = C ) by A1, A2, Th51;
then ( the_altitude (A,B,C) = Line (A,C) & the_altitude (B,C,A) = Line (B,C) ) by A3, A4, Th36;
then A5: ( C in the_altitude (A,B,C) & C in the_altitude (B,C,A) ) by EUCLID_4:41;
A6: C in the_altitude (C,A,B) by A3, Th30;
A7: (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {C}

proof

C in (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) by A5, XBOOLE_0:def 4;
hence (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {C} by EUCLID12:22, A1, A5, Th52; :: thesis: verum

end;

A8: (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {C}

proof

B,C,A is_a_triangle by A1, MENELAUS:15;
then A9: (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) is being_point by A5, A3, Th30, Th53;
C in (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) by A5, A6, XBOOLE_0:def 4;
hence (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {C} by A9, EUCLID12:22; :: thesis: verum

end;

(the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {C}

proof

C,A,B is_a_triangle by A1, MENELAUS:15;
then A10: (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) is being_point by A5, A3, Th30, Th54;
C in (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) by A5, A6, XBOOLE_0:def 4;
hence (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {C} by A10, EUCLID12:22; :: thesis: verum

end;

hence ( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {C} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {C} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {C} ) by A7, A8; :: thesis: verum