theorem Th36: :: EUCLID13:44

for A, B, C being Point of (TOP-REAL 2) st B <> C & not A in Line (B,C) holds
the_altitude (A,B,C) = Line (A,(the_foot_of_the_altitude (A,B,C)))