let A, B, C be Point of (TOP-REAL 2); :: thesis: ( B <> C implies the_altitude (A,B,C) is being_line )
assume B <> C ; :: thesis: the_altitude (A,B,C) is being_line
then consider L1, L2 being Element of line_of_REAL 2 such that
A1: the_altitude (A,B,C) = L1 and
L2 = Line (B,C) and
A in L1 and
A2: L1 _|_ L2 by Def1;
thus the_altitude (A,B,C) is being_line by A1, A2, EUCLIDLP:67; :: thesis: verum