let A, B, C be Point of (TOP-REAL 2); :: thesis: ( B <> C implies the_foot_of_the_altitude (A,B,C) = the_foot_of_the_altitude (A,C,B) )
assume A1: B <> C ; :: thesis: the_foot_of_the_altitude (A,B,C) = the_foot_of_the_altitude (A,C,B)
consider D being Point of (TOP-REAL 2) such that
A2: the_foot_of_the_altitude (A,B,C) = D and
A3: (the_altitude (A,B,C)) /\ (Line (B,C)) = {D} by A1, Def2;
consider E being Point of (TOP-REAL 2) such that
A4: the_foot_of_the_altitude (A,C,B) = E and
A5: (the_altitude (A,C,B)) /\ (Line (C,B)) = {E} by A1, Def2;
{D} = {E} by A3, A5, A1, Th32;
hence the_foot_of_the_altitude (A,B,C) = the_foot_of_the_altitude (A,C,B) by A2, A4, ZFMISC_1:3; :: thesis: verum