let A, B, C be Point of (TOP-REAL 2); :: thesis: ( B <> C & B <> A & angle (A,B,C) = PI / 2 implies the_foot_of_the_altitude (A,B,C) = B )
assume that
A1: B <> C and
A2: B <> A and
A3: angle (A,B,C) = PI / 2 ; :: thesis: the_foot_of_the_altitude (A,B,C) = B
|((A - B),(C - B))| = 0 by A1, A2, A3, EUCLID_3:45;
then |((B - A),(B - C))| = 0 by Th10;
hence the_foot_of_the_altitude (A,B,C) = B by A1, Th43; :: thesis: verum