:: deftheorem Def1 defines the_altitude EUCLID13:def 1 :
for A, B, C being Point of (TOP-REAL 2) st B <> C holds
for b₄ being Element of line_of_REAL 2 holds
( b₄ = the_altitude (A,B,C) iff ex L1, L2 being Element of line_of_REAL 2 st
( b₄ = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 ) );