let A, B, C be Point of (TOP-REAL 2); ( B <> C & not A in Line (B,C) implies the_altitude (A,B,C) = Line (A,(the_foot_of_the_altitude (A,B,C))) )
assume that
A1:
B <> C
and
A2:
not A in Line (B,C)
; the_altitude (A,B,C) = Line (A,(the_foot_of_the_altitude (A,B,C)))
consider L1, L2 being Element of line_of_REAL 2 such that
A3:
the_altitude (A,B,C) = L1
and
A4:
L2 = Line (B,C)
and
A5:
A in L1
and
A6:
L1 _|_ L2
by A1, Def1;
consider P being Point of (TOP-REAL 2) such that
A7:
the_foot_of_the_altitude (A,B,C) = P
and
A8:
(the_altitude (A,B,C)) /\ (Line (B,C)) = {P}
by A1, Def2;
reconsider rA = A, rP = P as Element of REAL 2 by EUCLID:22;
reconsider L3 = Line (rA,rP) as Element of line_of_REAL 2 by EUCLIDLP:47;
per cases
( A = P or A <> P )
;
suppose
A = P
;
the_altitude (A,B,C) = Line (A,(the_foot_of_the_altitude (A,B,C)))then
A in (the_altitude (A,B,C)) /\ (Line (B,C))
by A8, TARSKI:def 1;
hence
the_altitude (
A,
B,
C)
= Line (
A,
(the_foot_of_the_altitude (A,B,C)))
by A2, XBOOLE_0:def 4;
verum end; suppose A9:
A <> P
;
the_altitude (A,B,C) = Line (A,(the_foot_of_the_altitude (A,B,C)))
(
A in L1 &
P in L1 &
L1 is
being_line )
by A6, A3, A5, A1, A7, Th35, EUCLIDLP:67;
then
Line (
A,
P)
= L1
by A9, EUCLID12:49;
then
(
A in L3 &
L3 _|_ L2 )
by A6, EUCLID12:4, EUCLID_4:9;
then
(
L3 = the_altitude (
A,
B,
C) &
L3 = Line (
A,
P) )
by A1, A4, Def1, EUCLID12:4;
hence
the_altitude (
A,
B,
C)
= Line (
A,
(the_foot_of_the_altitude (A,B,C)))
by A7;
verum end; end;