let A, B, C be Point of (TOP-REAL 2); ( A,B,C is_a_triangle & |((C - A),(B - C))| = 0 implies ( (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} ) )
assume that
A1:
A,B,C is_a_triangle
and
A2:
|((C - A),(B - C))| = 0
; ( (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} )
A3:
A,B,C are_mutually_distinct
by A1, EUCLID_6:20;
B,C,A is_a_triangle
by A1, MENELAUS:15;
then A4:
( not A in Line (B,C) & not B in Line (C,A) )
by A1, Th20;
( the_foot_of_the_altitude (A,B,C) = C & the_foot_of_the_altitude (B,C,A) = C )
by A1, A2, Th51;
then
( the_altitude (A,B,C) = Line (A,C) & the_altitude (B,C,A) = Line (B,C) )
by A3, A4, Th36;
then A5:
( C in the_altitude (A,B,C) & C in the_altitude (B,C,A) )
by EUCLID_4:41;
A6:
C in the_altitude (C,A,B)
by A3, Th30;
A7:
(the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {C}
proof
C in (the_altitude (A,B,C)) /\ (the_altitude (B,C,A))
by A5, XBOOLE_0:def 4;
hence
(the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {C}
by EUCLID12:22, A1, A5, Th52;
verum
end;
A8:
(the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {C}
proof
B,
C,
A is_a_triangle
by A1, MENELAUS:15;
then A9:
(the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) is
being_point
by A5, A3, Th30, Th53;
C in (the_altitude (B,C,A)) /\ (the_altitude (C,A,B))
by A5, A6, XBOOLE_0:def 4;
hence
(the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {C}
by A9, EUCLID12:22;
verum
end;
(the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {C}
proof
C,
A,
B is_a_triangle
by A1, MENELAUS:15;
then A10:
(the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) is
being_point
by A5, A3, Th30, Th54;
C in (the_altitude (C,A,B)) /\ (the_altitude (A,B,C))
by A5, A6, XBOOLE_0:def 4;
hence
(the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {C}
by A10, EUCLID12:22;
verum
end;
hence
( (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 A7, A8; verum