theorem Th53: :: EUCLID13:64

for A, B, C being Point of (TOP-REAL 2) st B,C,A is_a_triangle & C in the_altitude (B,C,A) & C in the_altitude (C,A,B) holds
(the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) is being_point