:: deftheorem defines the_orthocenter EUCLID13:def 4 :
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
for b₄ being Point of (TOP-REAL 2) holds
( b₄ = the_orthocenter (A,B,C) iff ( (the_altitude (A,B,C)) /\ (the_altitude (B,C,A)) = {b₄} & (the_altitude (B,C,A)) /\ (the_altitude (C,A,B)) = {b₄} & (the_altitude (C,A,B)) /\ (the_altitude (A,B,C)) = {b₄} ) );