:: deftheorem Def2 defines the_foot_of_the_altitude EUCLID13:def 2 :
for A, B, C being Point of (TOP-REAL 2) st B <> C holds
for b₄ being Point of (TOP-REAL 2) holds
( b₄ = the_foot_of_the_altitude (A,B,C) iff ex P being Point of (TOP-REAL 2) st
( b₄ = P & (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} ) );