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
D = 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 D = 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: D = the_foot_of_the_altitude (A,B,C)
|((D - A),(D - C))| = 0 by A1, A2, A3, Th11;
then A5: D = the_foot_of_the_altitude (A,D,C) by A4, Th43;
reconsider rB = B, rC = C as Element of REAL 2 by EUCLID:22;
D in Line (B,C)

proof

D in Line (rC,rB) by A3;
hence D in Line (B,C) by EUCLID12:4; :: thesis: verum

end;

hence D = the_foot_of_the_altitude (A,B,C) by A1, A4, A5, Th42; :: thesis: verum