let A, B, C be Point of (TOP-REAL 2); :: thesis: ( B <> C implies ( the_foot_of_the_altitude (A,B,C) in Line (B,C) & the_foot_of_the_altitude (A,B,C) in the_altitude (A,B,C) ) )
assume B <> C ; :: thesis: ( the_foot_of_the_altitude (A,B,C) in Line (B,C) & the_foot_of_the_altitude (A,B,C) in the_altitude (A,B,C) )
then consider P being Point of (TOP-REAL 2) such that
A1: P = the_foot_of_the_altitude (A,B,C) and
A2: (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} by Def2;
P in {P} by TARSKI:def 1;
hence ( the_foot_of_the_altitude (A,B,C) in Line (B,C) & the_foot_of_the_altitude (A,B,C) in the_altitude (A,B,C) ) by A1, A2, XBOOLE_0:def 4; :: thesis: verum