let A, B, C be Point of (TOP-REAL 2); ( A,B,C is_a_triangle implies ex P being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {P} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {P} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {P} ) )
assume A1:
A,B,C is_a_triangle
; ex P being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {P} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {P} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {P} )
per cases
( |((C - A),(B - C))| = 0 or |((B - C),(A - B))| = 0 or |((C - A),(A - B))| = 0 or ( not |((C - A),(B - C))| = 0 & not |((B - C),(A - B))| = 0 & not |((C - A),(A - B))| = 0 ) )
;
suppose A2:
|((C - A),(B - C))| = 0
;
ex P being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {P} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {P} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {P} )take
C
;
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {C} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {C} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {C} )thus
(
(the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {C} &
(the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {C} &
(the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {C} )
by A1, A2, Th55;
verum end; suppose A3:
|((B - C),(A - B))| = 0
;
ex P being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {P} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {P} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {P} )take
B
;
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {B} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {B} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {B} )
C,
A,
B is_a_triangle
by A1, MENELAUS:15;
hence
(
(the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {B} &
(the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {B} &
(the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {B} )
by A3, Th55;
verum end; suppose A4:
|((C - A),(A - B))| = 0
;
ex P being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {P} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {P} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {P} )take
A
;
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {A} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {A} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {A} )
B,
C,
A is_a_triangle
by A1, MENELAUS:15;
hence
(
(the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {A} &
(the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {A} &
(the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {A} )
by A4, Th55;
verum end; suppose
( not
|((C - A),(B - C))| = 0 & not
|((B - C),(A - B))| = 0 & not
|((C - A),(A - B))| = 0 )
;
ex P being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {P} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {P} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {P} )then A5:
Line (
A,
(the_foot_of_the_altitude (A,B,C))),
Line (
C,
(the_foot_of_the_altitude (C,A,B))),
Line (
B,
(the_foot_of_the_altitude (B,C,A)))
are_concurrent
by A1, Th50;
A6:
A,
B,
C are_mutually_distinct
by A1, EUCLID_6:20;
A7:
(
B,
C,
A is_a_triangle &
C,
A,
B is_a_triangle )
by A1, MENELAUS:15;
then
( not
A in Line (
B,
C) & not
B in Line (
C,
A) & not
C in Line (
A,
B) )
by A1, Th20;
then A8:
(
the_altitude (
A,
B,
C)
= Line (
A,
(the_foot_of_the_altitude (A,B,C))) &
the_altitude (
C,
A,
B)
= Line (
C,
(the_foot_of_the_altitude (C,A,B))) &
the_altitude (
B,
C,
A)
= Line (
B,
(the_foot_of_the_altitude (B,C,A))) )
by A6, Th36;
consider L1,
L2 being
Element of
line_of_REAL 2
such that A9:
the_altitude (
A,
B,
C)
= L1
and A10:
L2 = Line (
B,
C)
and
A in L1
and A11:
L1 _|_ L2
by A6, Def1;
consider L3,
L4 being
Element of
line_of_REAL 2
such that A12:
the_altitude (
C,
A,
B)
= L3
and A13:
L4 = Line (
A,
B)
and
C in L3
and A14:
L3 _|_ L4
by A6, Def1;
consider L5,
L6 being
Element of
line_of_REAL 2
such that A15:
the_altitude (
B,
C,
A)
= L5
and A16:
L6 = Line (
C,
A)
and
B in L5
and A17:
L5 _|_ L6
by A6, Def1;
A18:
not
Line (
A,
(the_foot_of_the_altitude (A,B,C)))
is_parallel_to Line (
C,
(the_foot_of_the_altitude (C,A,B)))
proof
assume A19:
Line (
A,
(the_foot_of_the_altitude (A,B,C)))
is_parallel_to Line (
C,
(the_foot_of_the_altitude (C,A,B)))
;
contradiction
(
L1 is
being_line &
L3 is
being_line &
L1,
L3 are_coplane )
by A9, A12, A6, Th31, EUCLID12:39;
then
L1 // L3
by A19, A8, A9, A12, EUCLIDLP:113;
then
L1 _|_ L4
by A14, EUCLIDLP:61;
then A20:
L2 // L4
by A11, EUCLIDLP:111, EUCLID12:16;
(
B in L2 &
B in L4 )
by A10, A13, EUCLID_4:41;
then
Line (
A,
B)
= Line (
B,
C)
by A10, A13, A20, XBOOLE_0:3, EUCLIDLP:71;
then
C in Line (
A,
B)
by EUCLID_4:41;
hence
contradiction
by A7, A6, MENELAUS:13;
verum
end; consider D being
Point of
(TOP-REAL 2) such that A21:
D in the_altitude (
A,
B,
C)
and A22:
D in the_altitude (
C,
A,
B)
and A23:
D in the_altitude (
B,
C,
A)
by A8, A18, A5, MENELAUS:def 1;
A24:
(
D in L1 /\ L3 &
D in L1 /\ L5 &
D in L3 /\ L5 )
by A21, A22, A23, A9, A12, A15, XBOOLE_0:def 4;
A25:
(
L1 meets L3 &
L1 meets L5 &
L3 meets L5 )
by A21, A22, A23, A9, A12, A15, XBOOLE_0:def 4;
L1 <> L3
proof
assume
L1 = L3
;
contradiction
then A26:
L2 // L4
by A14, A11, EUCLIDLP:111, EUCLID12:16;
(
B in L2 &
B in L4 )
by A10, A13, EUCLID_4:41;
then
L2 = L4
by A26, XBOOLE_0:3, EUCLIDLP:71;
then
C in Line (
A,
B)
by A10, A13, EUCLID_4:41;
hence
contradiction
by A7, A6, MENELAUS:13;
verum
end; then A27:
not
L1 // L3
by A25, EUCLIDLP:71;
( not
L1 is
being_point & not
L3 is
being_point )
by A9, A12, A6, Th31, EUCLID12:9;
then A28:
L1 /\ L3 = {D}
by A24, EUCLID12:22, A27, EUCLID12:21;
L1 <> L5
proof
assume
L1 = L5
;
contradiction
then A29:
L2 // L6
by A17, A11, EUCLIDLP:111, EUCLID12:16;
(
C in L2 &
C in L6 )
by A16, A10, EUCLID_4:41;
then
L2 = L6
by A29, XBOOLE_0:3, EUCLIDLP:71;
then
A in Line (
B,
C)
by A16, A10, EUCLID_4:41;
hence
contradiction
by A1, A6, MENELAUS:13;
verum
end; then A30:
not
L1 // L5
by A25, EUCLIDLP:71;
( not
L1 is
being_point & not
L5 is
being_point )
by A15, A9, A6, Th31, EUCLID12:9;
then A31:
L1 /\ L5 = {D}
by A24, EUCLID12:22, A30, EUCLID12:21;
L3 <> L5
proof
assume
L3 = L5
;
contradiction
then A32:
L4 // L6
by A17, A14, EUCLIDLP:111, EUCLID12:16;
(
A in L4 &
A in L6 )
by A16, A13, EUCLID_4:41;
then
Line (
A,
B)
= Line (
C,
A)
by A16, A13, A32, XBOOLE_0:3, EUCLIDLP:71;
then
C in Line (
A,
B)
by EUCLID_4:41;
hence
contradiction
by A7, A6, MENELAUS:13;
verum
end; then A33:
not
L3 // L5
by A25, EUCLIDLP:71;
( not
L3 is
being_point & not
L5 is
being_point )
by A15, A12, A6, Th31, EUCLID12:9;
then
L3 /\ L5 = {D}
by A24, EUCLID12:22, A33, EUCLID12:21;
hence
ex
P being
Point of
(TOP-REAL 2) st
(
(the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {P} &
(the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {P} &
(the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {P} )
by A28, A31, A9, A12, A15;
verum end;