let r be Real; 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); ( 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
; 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; verum