let A, B, C be Point of (TOP-REAL 2); :: thesis: ( B <> C implies A in the_altitude (A,B,C) )
assume B <> C ; :: thesis: A in the_altitude (A,B,C)
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
A2: A in L1 and
L1 _|_ L2 by Def1;
thus A in the_altitude (A,B,C) by A1, A2; :: thesis: verum