let A, B, C, D be Point of (TOP-REAL 2); :: thesis: ( B <> C & D in the_altitude (A,B,C) implies the_altitude (D,B,C) = the_altitude (A,B,C) )
assume that
A1: B <> C and
A2: D in the_altitude (A,B,C) ; :: thesis: the_altitude (D,B,C) = 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
A in L1 and
A5: L1 _|_ L2 by A1, Def1;
consider L11, L12 being Element of line_of_REAL 2 such that
A6: the_altitude (D,B,C) = L11 and
A7: L12 = Line (B,C) and
A8: D in L11 and
A9: L11 _|_ L12 by A1, Def1;
( L1 // L11 & D in L1 & D in L11 ) by A2, A3, A8, A4, A7, A5, A9, EUCLID12:16, EUCLIDLP:111;
hence the_altitude (D,B,C) = the_altitude (A,B,C) by A3, A6, EUCLIDLP:71, XBOOLE_0:3; :: thesis: verum