let A, B, C, D be Point of (TOP-REAL 2); ( B <> C & D in Line (B,C) & D <> C implies the_altitude (A,B,C) = the_altitude (A,D,C) )
assume that
A1:
B <> C
and
A2:
D in Line (B,C)
and
A3:
D <> C
; the_altitude (A,B,C) = the_altitude (A,D,C)
consider L1, L2 being Element of line_of_REAL 2 such that
A4:
the_altitude (A,B,C) = L1
and
A5:
L2 = Line (B,C)
and
A6:
A in L1
and
A7:
L1 _|_ L2
by A1, Def1;
consider L3, L4 being Element of line_of_REAL 2 such that
A8:
the_altitude (A,D,C) = L3
and
A9:
L4 = Line (D,C)
and
A10:
A in L3
and
A11:
L3 _|_ L4
by A3, Def1;
A12:
L2 = L4
by A2, A3, A5, A9, Th7;
L1 meets L3
by A6, A10, XBOOLE_0:def 4;
hence
the_altitude (A,B,C) = the_altitude (A,D,C)
by A4, A8, A7, A11, A12, EUCLIDLP:111, EUCLID12:16, EUCLIDLP:71; verum