let A, B, C be Point of (TOP-REAL 2); ( 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
; 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
;
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;
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
;
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;
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
;
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;
verum
end;
hence
the_foot_of_the_altitude (A,B,C),B,A is_a_triangle
by A11, A13, A14, EUCLID_6:20; verum