theorem :: EUCLID13:40

for A, B, C, D being Point of (TOP-REAL 2) st B <> C & D in the_altitude (A,B,C) holds
the_altitude (D,B,C) = the_altitude (A,B,C)