let A, B, C be Point of (TOP-REAL 2); :: thesis: ( B <> C implies |((A - (the_foot_of_the_altitude (A,B,C))),(B - C))| = 0 )
assume A1: B <> C ; :: thesis: |((A - (the_foot_of_the_altitude (A,B,C))),(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 ( not A in Line (B,C) or A in Line (B,C) ) ;
suppose not A in Line (B,C) ; :: thesis: |((A - (the_foot_of_the_altitude (A,B,C))),(B - C))| = 0
then ( L1 _|_ L2 & L1 = Line (A,(the_foot_of_the_altitude (A,B,C))) & L2 = Line (B,C) ) by A1, A2, A3, Th36;
hence |((A - (the_foot_of_the_altitude (A,B,C))),(B - C))| = 0 by EUCLID12:48; :: thesis: verum
end;
suppose A in Line (B,C) ; :: thesis: |((A - (the_foot_of_the_altitude (A,B,C))),(B - C))| = 0
then A4: the_foot_of_the_altitude (A,B,C) = A by A1, Th37;
|((A - (the_foot_of_the_altitude (A,B,C))),(B - C))| = |(A,(B - C))| - |((the_foot_of_the_altitude (A,B,C)),(B - C))| by EUCLID_2:27
.= 0 by A4 ;
hence |((A - (the_foot_of_the_altitude (A,B,C))),(B - C))| = 0 ; :: thesis: verum
end;
end;