let A, B, C be Point of (TOP-REAL 2); ( A,B,C is_a_triangle & C in the_altitude (A,B,C) & C in the_altitude (B,C,A) implies (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) is being_point )
assume that
A1:
A,B,C is_a_triangle
and
A2:
C in the_altitude (A,B,C)
and
A3:
C in the_altitude (B,C,A)
; (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) is being_point
A4:
A,B,C are_mutually_distinct
by A1, EUCLID_6:20;
consider L1, L2 being Element of line_of_REAL 2 such that
A5:
the_altitude (A,B,C) = L1
and
A6:
L2 = Line (B,C)
and
A in L1
and
A7:
L1 _|_ L2
by A4, Def1;
consider L3, L4 being Element of line_of_REAL 2 such that
A8:
the_altitude (B,C,A) = L3
and
A9:
L4 = Line (C,A)
and
B in L3
and
A10:
L3 _|_ L4
by A4, Def1;
A11:
not L1 // L3
proof
assume A12:
L1 // L3
;
contradiction
L1 <> L3
proof
assume
L1 = L3
;
contradiction
then
(
L1 _|_ L2 &
L1 _|_ L4 &
C in L1 &
C in L2 &
C in L4 )
by A6, A9, A7, A10, A2, A5, EUCLID_4:41;
then
L2 = L4
by EUCLID12:16, EUCLIDLP:108;
then
A in Line (
B,
C)
by A6, A9, EUCLID_4:41;
hence
contradiction
by A1, A4, MENELAUS:13;
verum
end;
hence
contradiction
by XBOOLE_0:3, A12, EUCLIDLP:71, A5, A8, A2, A3;
verum
end;
( not L1 is being_point & not L3 is being_point )
by A4, A5, A8, Th31, EUCLID12:9;
hence
(the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) is being_point
by A5, A8, A11, EUCLID12:21; verum