let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & not |((C - A),(B - C))| is zero & not |((B - C),(A - B))| is zero & not |((C - A),(A - B))| is zero implies 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 )
assume that
A1: A,B,C is_a_triangle and
A2: ( not |((C - A),(B - C))| is zero & not |((B - C),(A - B))| is zero & not |((C - A),(A - B))| is zero ) ; :: thesis: 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
A3: A,B,C are_mutually_distinct by A1, EUCLID_6:20;
set r = - ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|);
set s = - ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|);
set t = - ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|);
set D = ((- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)) * B) + ((1 - (- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|))) * C);
set E = ((- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)) * C) + ((1 - (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|))) * A);
set F = ((- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|)) * A) + ((1 - (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))) * B);
( ((- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)) * B) + ((1 - (- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|))) * C) <> C & ((- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)) * C) + ((1 - (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|))) * A) <> A & ((- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|)) * A) + ((1 - (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))) * B) <> B )

proof

assume ( not ((- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)) * B) + ((1 - (- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|))) * C) <> C or not ((- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)) * C) + ((1 - (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|))) * A) <> A or not ((- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|)) * A) + ((1 - (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))) * B) <> B ) ; :: thesis: contradiction
then A4: ( C = the_foot_of_the_altitude (A,B,C) or A = the_foot_of_the_altitude (B,C,A) or B = the_foot_of_the_altitude (C,A,B) ) by A3, Th49;
( |((A - C),(B - C))| = - |((C - A),(B - C))| & |((B - A),(C - A))| = - |((C - A),(A - B))| & |((C - B),(A - B))| = - |((B - C),(A - B))| ) by Th16;
hence contradiction by A4, A2, A3, Th38ThJ8; :: thesis: verum

end;

then A5: ( ((- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)) * B) + ((1 - (- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|))) * C) = the_foot_of_the_altitude (A,B,C) & ((- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)) * C) + ((1 - (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|))) * A) = the_foot_of_the_altitude (B,C,A) & ((- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|)) * A) + ((1 - (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))) * B) = the_foot_of_the_altitude (C,A,B) ) by A3, Th48;
(((((- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)) / (1 - (- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)))) * (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|))) / (1 - (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)))) * (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))) / (1 - (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))) = 1 by A3, A2, Th17;
then A6: (((- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)) / (1 - (- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)))) * ((- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|)) / (1 - (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))))) * ((- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)) / (1 - (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)))) = 1 ;
A7: A,C,B is_a_triangle by A1, MENELAUS:15;
( - ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) <> 1 & - ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|) <> 1 & - ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|) <> 1 )

proof

assume ( not - ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) <> 1 or not - ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|) <> 1 or not - ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|) <> 1 ) ; :: thesis: contradiction
then ( ( - ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) = 1 & B <> C & - ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) = - ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) & ((- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)) * B) + ((1 - (- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|))) * C) = ((- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|)) * B) + ((1 - (- ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|))) * C) ) or ( - ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|) = 1 & C <> A & - ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|) = - ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|) & ((- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)) * C) + ((1 - (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|))) * A) = ((- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|)) * C) + ((1 - (- ((((|(C,A)| - |(A,A)|) - |(B,C)|) + |(B,A)|) / |((C - A),(C - A))|))) * A) ) or ( - ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|) = 1 & A <> B & - ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|) = - ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|) & ((- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|)) * A) + ((1 - (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))) * B) = ((- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|)) * A) + ((1 - (- ((((|(A,B)| - |(B,B)|) - |(C,A)|) + |(C,B)|) / |((A - B),(A - B))|))) * B) ) ) ;
hence contradiction by A2, Th19; :: thesis: verum

end;

hence 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 A5, A6, A7, MENELAUS:22; :: thesis: verum