let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle implies ex P being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {P} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {P} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {P} ) )
assume A1: A,B,C is_a_triangle ; :: thesis: ex P being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {P} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {P} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {P} )

per cases ( |((C - A),(B - C))| = 0 or |((B - C),(A - B))| = 0 or |((C - A),(A - B))| = 0 or ( not |((C - A),(B - C))| = 0 & not |((B - C),(A - B))| = 0 & not |((C - A),(A - B))| = 0 ) ) ;

suppose A2: |((C - A),(B - C))| = 0 ; :: thesis: ex P being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {P} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {P} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {P} )

take C ; :: 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} )
thus ( (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 A1, A2, Th55; :: thesis: verum

end;

suppose A3: |((B - C),(A - B))| = 0 ; :: thesis: ex P being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {P} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {P} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {P} )

take B ; :: thesis: ( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {B} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {B} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {B} )
C,A,B is_a_triangle by A1, MENELAUS:15;
hence ( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {B} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {B} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {B} ) by A3, Th55; :: thesis: verum

end;

suppose A4: |((C - A),(A - B))| = 0 ; :: thesis: ex P being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {P} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {P} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {P} )

take A ; :: thesis: ( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {A} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {A} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {A} )
B,C,A is_a_triangle by A1, MENELAUS:15;
hence ( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {A} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {A} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {A} ) by A4, Th55; :: thesis: verum

end;

suppose ( not |((C - A),(B - C))| = 0 & not |((B - C),(A - B))| = 0 & not |((C - A),(A - B))| = 0 ) ; :: thesis: ex P being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {P} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {P} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {P} )

then A5: Line (A,(the_foot_of_the_altitude (A,B,C))), Line (C,(the_foot_of_the_altitude (C,A,B))), Line (B,(the_foot_of_the_altitude (B,C,A))) are_concurrent by A1, Th50;
A6: A,B,C are_mutually_distinct by A1, EUCLID_6:20;
A7: ( B,C,A is_a_triangle & C,A,B is_a_triangle ) by A1, MENELAUS:15;
then ( not A in Line (B,C) & not B in Line (C,A) & not C in Line (A,B) ) by A1, Th20;
then A8: ( the_altitude (A,B,C) = Line (A,(the_foot_of_the_altitude (A,B,C))) & the_altitude (C,A,B) = Line (C,(the_foot_of_the_altitude (C,A,B))) & the_altitude (B,C,A) = Line (B,(the_foot_of_the_altitude (B,C,A))) ) by A6, Th36;
consider L1, L2 being Element of line_of_REAL 2 such that
A9: the_altitude (A,B,C) = L1 and
A10: L2 = Line (B,C) and
A in L1 and
A11: L1 _|_ L2 by A6, Def1;
consider L3, L4 being Element of line_of_REAL 2 such that
A12: the_altitude (C,A,B) = L3 and
A13: L4 = Line (A,B) and
C in L3 and
A14: L3 _|_ L4 by A6, Def1;
consider L5, L6 being Element of line_of_REAL 2 such that
A15: the_altitude (B,C,A) = L5 and
A16: L6 = Line (C,A) and
B in L5 and
A17: L5 _|_ L6 by A6, Def1;
A18: not Line (A,(the_foot_of_the_altitude (A,B,C))) is_parallel_to Line (C,(the_foot_of_the_altitude (C,A,B)))

proof

assume A19: Line (A,(the_foot_of_the_altitude (A,B,C))) is_parallel_to Line (C,(the_foot_of_the_altitude (C,A,B))) ; :: thesis: contradiction
( L1 is being_line & L3 is being_line & L1,L3 are_coplane ) by A9, A12, A6, Th31, EUCLID12:39;
then L1 // L3 by A19, A8, A9, A12, EUCLIDLP:113;
then L1 _|_ L4 by A14, EUCLIDLP:61;
then A20: L2 // L4 by A11, EUCLIDLP:111, EUCLID12:16;
( B in L2 & B in L4 ) by A10, A13, EUCLID_4:41;
then Line (A,B) = Line (B,C) by A10, A13, A20, XBOOLE_0:3, EUCLIDLP:71;
then C in Line (A,B) by EUCLID_4:41;
hence contradiction by A7, A6, MENELAUS:13; :: thesis: verum

end;

consider D being Point of (TOP-REAL 2) such that
A21: D in the_altitude (A,B,C) and
A22: D in the_altitude (C,A,B) and
A23: D in the_altitude (B,C,A) by A8, A18, A5, MENELAUS:def 1;
A24: ( D in L1 /\ L3 & D in L1 /\ L5 & D in L3 /\ L5 ) by A21, A22, A23, A9, A12, A15, XBOOLE_0:def 4;
A25: ( L1 meets L3 & L1 meets L5 & L3 meets L5 ) by A21, A22, A23, A9, A12, A15, XBOOLE_0:def 4;
L1 <> L3

proof

assume L1 = L3 ; :: thesis: contradiction
then A26: L2 // L4 by A14, A11, EUCLIDLP:111, EUCLID12:16;
( B in L2 & B in L4 ) by A10, A13, EUCLID_4:41;
then L2 = L4 by A26, XBOOLE_0:3, EUCLIDLP:71;
then C in Line (A,B) by A10, A13, EUCLID_4:41;
hence contradiction by A7, A6, MENELAUS:13; :: thesis: verum

end;

then A27: not L1 // L3 by A25, EUCLIDLP:71;
( not L1 is being_point & not L3 is being_point ) by A9, A12, A6, Th31, EUCLID12:9;
then A28: L1 /\ L3 = {D} by A24, EUCLID12:22, A27, EUCLID12:21;
L1 <> L5

proof

assume L1 = L5 ; :: thesis: contradiction
then A29: L2 // L6 by A17, A11, EUCLIDLP:111, EUCLID12:16;
( C in L2 & C in L6 ) by A16, A10, EUCLID_4:41;
then L2 = L6 by A29, XBOOLE_0:3, EUCLIDLP:71;
then A in Line (B,C) by A16, A10, EUCLID_4:41;
hence contradiction by A1, A6, MENELAUS:13; :: thesis: verum

end;

then A30: not L1 // L5 by A25, EUCLIDLP:71;
( not L1 is being_point & not L5 is being_point ) by A15, A9, A6, Th31, EUCLID12:9;
then A31: L1 /\ L5 = {D} by A24, EUCLID12:22, A30, EUCLID12:21;
L3 <> L5

proof

assume L3 = L5 ; :: thesis: contradiction
then A32: L4 // L6 by A17, A14, EUCLIDLP:111, EUCLID12:16;
( A in L4 & A in L6 ) by A16, A13, EUCLID_4:41;
then Line (A,B) = Line (C,A) by A16, A13, A32, XBOOLE_0:3, EUCLIDLP:71;
then C in Line (A,B) by EUCLID_4:41;
hence contradiction by A7, A6, MENELAUS:13; :: thesis: verum

end;

then A33: not L3 // L5 by A25, EUCLIDLP:71;
( not L3 is being_point & not L5 is being_point ) by A15, A12, A6, Th31, EUCLID12:9;
then L3 /\ L5 = {D} by A24, EUCLID12:22, A33, EUCLID12:21;
hence ex P being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {P} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {P} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {P} ) by A28, A31, A9, A12, A15; :: thesis: verum

end;

end;