let A, B, C be Point of (TOP-REAL 2); :: thesis: ( B <> C implies |((A - (the_foot_of_the_altitude (A,B,C))),(B - (the_foot_of_the_altitude (A,B,C))))| = 0 )
assume A1: B <> C ; :: thesis: |((A - (the_foot_of_the_altitude (A,B,C))),(B - (the_foot_of_the_altitude (A,B,C))))| = 0
consider L1, L2 being Element of line_of_REAL 2 such that
A2: the_altitude (A,B,C) = L1 and
A3: ( L2 = Line (B,C) & A in L1 & L1 _|_ L2 ) by A1, Def1;
per cases ( B = the_foot_of_the_altitude (A,B,C) or B <> the_foot_of_the_altitude (A,B,C) ) ;
suppose A4: B = the_foot_of_the_altitude (A,B,C) ; :: thesis: |((A - (the_foot_of_the_altitude (A,B,C))),(B - (the_foot_of_the_altitude (A,B,C))))| = 0
|((A - (the_foot_of_the_altitude (A,B,C))),(B - (the_foot_of_the_altitude (A,B,C))))| = |((A - (the_foot_of_the_altitude (A,B,C))),B)| - |((A - (the_foot_of_the_altitude (A,B,C))),(the_foot_of_the_altitude (A,B,C)))| by EUCLID_2:27;
hence |((A - (the_foot_of_the_altitude (A,B,C))),(B - (the_foot_of_the_altitude (A,B,C))))| = 0 by A4; :: thesis: verum
end;
suppose A5: B <> the_foot_of_the_altitude (A,B,C) ; :: thesis: |((A - (the_foot_of_the_altitude (A,B,C))),(B - (the_foot_of_the_altitude (A,B,C))))| = 0
A6: L2 is being_line by A3, EUCLIDLP:67;
( the_foot_of_the_altitude (A,B,C) in Line (B,C) & B in Line (B,C) & C in Line (B,C) ) by EUCLID_4:41, A1, Th35;
then A7: Line (B,C) = Line (B,(the_foot_of_the_altitude (A,B,C))) by A6, A5, A3, EUCLID12:49;
per cases ( not A in Line (B,C) or A in Line (B,C) ) ;
end;
end;
end;