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