theorem Th56: :: EUCLID13:67

for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
ex P being Point of (TOP-REAL 2) st
( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {P} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {P} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {P} )