let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & |((C - A),(B - C))| is zero implies ( the_foot_of_the_altitude (A,B,C) = C & the_foot_of_the_altitude (B,C,A) = C ) )
assume that
A1: A,B,C is_a_triangle and
A2: |((C - A),(B - C))| is zero ; :: thesis: ( the_foot_of_the_altitude (A,B,C) = C & the_foot_of_the_altitude (B,C,A) = C )
A3: A,B,C are_mutually_distinct by A1, EUCLID_6:20;
A4: - |((C - A),(B - C))| = |((C - B),(C - A))| by Th14;
|((C - A),(C - B))| = - |((C - A),(B - C))| by Th14;
then the_foot_of_the_altitude (A,C,B) = C by A2, A3, Th43;
hence ( the_foot_of_the_altitude (A,B,C) = C & the_foot_of_the_altitude (B,C,A) = C ) by A2, A3, A4, Th43, Th34; :: thesis: verum