let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A,B,C is_a_triangle & |((B - A),(B - C))| <> 0 implies the_foot_of_the_altitude (A,B,C),B,A is_a_triangle )
assume that
A1: A,B,C is_a_triangle and
A2: |((B - A),(B - C))| <> 0 ; :: thesis: the_foot_of_the_altitude (A,B,C),B,A is_a_triangle
A3: A,B,C are_mutually_distinct by A1, EUCLID_6:20;
set p = the_foot_of_the_altitude (A,B,C);
consider P being Point of (TOP-REAL 2) such that
A4: the_foot_of_the_altitude (A,B,C) = P and
A5: (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} by A3, Def2;
consider L1, L2 being Element of line_of_REAL 2 such that
A6: the_altitude (A,B,C) = L1 and
A7: L2 = Line (B,C) and
A8: A in L1 and
L1 _|_ L2 by A3, Def1;
A9: P <> B by A4, A3, A2, Th41;
A10: the_foot_of_the_altitude (A,B,C) <> A by A1, Th44;
A11: the_foot_of_the_altitude (A,B,C),B,A are_mutually_distinct by A3, A2, Th41, A1, Th44;
P in Line (B,C) by A4, A3, Th35;
then ( B in Line (B,P) & C in Line (B,P) ) by A9, Th8, EUCLID_4:41;
then A12: Line (B,P) c= Line (B,C) by A3, EUCLID_4:43;
A13: angle ((the_foot_of_the_altitude (A,B,C)),B,A) <> PI
proof
assume angle ((the_foot_of_the_altitude (A,B,C)),B,A) = PI ; :: thesis: contradiction
then B in LSeg ((the_foot_of_the_altitude (A,B,C)),A) by EUCLID_6:11;
then B in Line (P,A) by A4, MENELAUS:12;
then A in Line (B,P) by A3, A2, Th41, A4, Th8;
then A in L1 /\ L2 by A12, A8, A7, XBOOLE_0:def 4;
hence contradiction by A5, A6, A7, A4, A10, TARSKI:def 1; :: thesis: verum
end;
A14: angle (B,A,(the_foot_of_the_altitude (A,B,C))) <> PI
proof
assume angle (B,A,(the_foot_of_the_altitude (A,B,C))) = PI ; :: thesis: contradiction
then A in LSeg (B,(the_foot_of_the_altitude (A,B,C))) by EUCLID_6:11;
then ( A in L1 & A in L2 ) by A12, A8, A7, A4, MENELAUS:12;
then A in L1 /\ L2 by XBOOLE_0:def 4;
hence contradiction by A4, A10, A5, A6, A7, TARSKI:def 1; :: thesis: verum
end;
angle (A,(the_foot_of_the_altitude (A,B,C)),B) <> PI
proof
assume angle (A,(the_foot_of_the_altitude (A,B,C)),B) = PI ; :: thesis: contradiction
then the_foot_of_the_altitude (A,B,C) in LSeg (A,B) by EUCLID_6:11;
then P in Line (A,B) by A4, MENELAUS:12;
then A in Line (B,P) by A9, Th8;
then A in L1 /\ L2 by A12, A8, A7, XBOOLE_0:def 4;
then A = P by A5, A6, A7, TARSKI:def 1;
hence contradiction by A4, A1, Th44; :: thesis: verum
end;
hence the_foot_of_the_altitude (A,B,C),B,A is_a_triangle by A11, A13, A14, EUCLID_6:20; :: thesis: verum