let A, B, C be Point of (TOP-REAL 2); :: thesis: ( B <> C & B = the_foot_of_the_altitude (A,B,C) implies |((B - A),(B - C))| = 0 )
assume that
A1: B <> C and
A2: B = the_foot_of_the_altitude (A,B,C) ; :: thesis: |((B - A),(B - C))| = 0
set ph = the_foot_of_the_altitude (A,B,C);
per cases ( A,B,C is_a_triangle or not A,B,C is_a_triangle ) ;
suppose A,B,C is_a_triangle ; :: thesis: |((B - A),(B - C))| = 0
|((A - (the_foot_of_the_altitude (A,B,C))),(C - (the_foot_of_the_altitude (A,B,C))))| = 0 by A1, Th40;
hence |((B - A),(B - C))| = 0 by A2, Th10; :: thesis: verum
end;
suppose A4: not A,B,C is_a_triangle ; :: thesis: |((B - A),(B - C))| = 0
consider P being Point of (TOP-REAL 2) such that
A5: the_foot_of_the_altitude (A,B,C) = P and
A6: (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} by A1, Def2;
consider L1, L2 being Element of line_of_REAL 2 such that
A7: the_altitude (A,B,C) = L1 and
L2 = Line (B,C) and
A8: A in L1 and
L1 _|_ L2 by A1, Def1;
( A in Line (B,C) & B in Line (B,C) & A in the_altitude (A,B,C) & B in the_altitude (A,B,C) ) by A1, A4, MENELAUS:13, A7, A8, Th35, A2;
then A in {(the_foot_of_the_altitude (A,B,C))} by A5, A6, XBOOLE_0:def 4;
then A11: A = B by A2, TARSKI:def 1;
|((B - A),(B - C))| = |(B,(B - C))| - |(A,(B - C))| by EUCLID_2:24
.= 0 by A11 ;
hence |((B - A),(B - C))| = 0 ; :: thesis: verum
end;
end;