theorem Th55: :: EUCLID13:66

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