let A, B, C be Point of (TOP-REAL 2); :: thesis: ( B <> C & not A in Line (B,C) implies the_altitude (A,B,C) = Line (A,(the_foot_of_the_altitude (A,B,C))) )
assume that
A1: B <> C and
A2: not A in Line (B,C) ; :: thesis: the_altitude (A,B,C) = Line (A,(the_foot_of_the_altitude (A,B,C)))
consider L1, L2 being Element of line_of_REAL 2 such that
A3: the_altitude (A,B,C) = L1 and
A4: L2 = Line (B,C) and
A5: A in L1 and
A6: L1 _|_ L2 by A1, Def1;
consider P being Point of (TOP-REAL 2) such that
A7: the_foot_of_the_altitude (A,B,C) = P and
A8: (the_altitude (A,B,C)) /\ (Line (B,C)) = {P} by A1, Def2;
reconsider rA = A, rP = P as Element of REAL 2 by EUCLID:22;
reconsider L3 = Line (rA,rP) as Element of line_of_REAL 2 by EUCLIDLP:47;
per cases ( A = P or A <> P ) ;
suppose A = P ; :: thesis: the_altitude (A,B,C) = Line (A,(the_foot_of_the_altitude (A,B,C)))
then A in (the_altitude (A,B,C)) /\ (Line (B,C)) by A8, TARSKI:def 1;
hence the_altitude (A,B,C) = Line (A,(the_foot_of_the_altitude (A,B,C))) by A2, XBOOLE_0:def 4; :: thesis: verum
end;
suppose A9: A <> P ; :: thesis: the_altitude (A,B,C) = Line (A,(the_foot_of_the_altitude (A,B,C)))
( A in L1 & P in L1 & L1 is being_line ) by A6, A3, A5, A1, A7, Th35, EUCLIDLP:67;
then Line (A,P) = L1 by A9, EUCLID12:49;
then ( A in L3 & L3 _|_ L2 ) by A6, EUCLID12:4, EUCLID_4:9;
then ( L3 = the_altitude (A,B,C) & L3 = Line (A,P) ) by A1, A4, Def1, EUCLID12:4;
hence the_altitude (A,B,C) = Line (A,(the_foot_of_the_altitude (A,B,C))) by A7; :: thesis: verum
end;
end;