let r be Real; :: thesis: for A, B, C, D being Point of (TOP-REAL 2) st B <> C & r = - ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) & D = (r * B) + ((1 - r) * C) & D = C holds
C = the_foot_of_the_altitude (A,B,C)
let A, B, C, D be Point of (TOP-REAL 2); :: thesis: ( B <> C & r = - ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) & D = (r * B) + ((1 - r) * C) & D = C implies C = the_foot_of_the_altitude (A,B,C) )
assume that
A1: B <> C and
A2: r = - ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) and
A3: D = (r * B) + ((1 - r) * C) and
A4: D = C ; :: thesis: C = the_foot_of_the_altitude (A,B,C)
reconsider rB = B, rC = C as Element of REAL 2 by EUCLID:22;
reconsider n = 2 as Nat ;
A5: rB - rC <> 0* n by A1, EUCLIDLP:9;
0 = - ((((|(B,C)| - |(C,C)|) - |(A,B)|) + |(A,C)|) / |((B - C),(B - C))|) by A2, A1, A3, A4, Th12;
then 0 * |((B - C),(B - C))| = - ((|((C - A),(B - C))| / |((B - C),(B - C))|) * |((B - C),(B - C))|) by Th13;
then 0 = - |((C - A),(B - C))| by A5, EUCLID_4:17, XCMPLX_1:87;
then |((C - A),(C - B))| = 0 by Th14;
then C = the_foot_of_the_altitude (A,C,B) by A1, Th43;
hence C = the_foot_of_the_altitude (A,B,C) by A1, Th34; :: thesis: verum