let A, B, C be Point of (TOP-REAL 2); :: thesis: ( B <> C implies the_altitude (A,B,C) = the_altitude (A,C,B) )
assume A1: B <> C ; :: thesis: the_altitude (A,B,C) = the_altitude (A,C,B)
then consider L11, L12 being Element of line_of_REAL 2 such that
A2: the_altitude (A,B,C) = L11 and
A3: L12 = Line (B,C) and
A4: A in L11 and
A5: L11 _|_ L12 by Def1;
consider L21, L22 being Element of line_of_REAL 2 such that
A6: the_altitude (A,C,B) = L21 and
A7: L22 = Line (C,B) and
A8: A in L21 and
A9: L21 _|_ L22 by A1, Def1;
L11 // L21 by A5, A9, A3, A7, EUCLID12:16, EUCLIDLP:111;
hence the_altitude (A,B,C) = the_altitude (A,C,B) by A2, A6, A4, A8, XBOOLE_0:3, EUCLIDLP:71; :: thesis: verum