let A, B, C be Point of (TOP-REAL 2); :: thesis: for L1, L2 being Element of line_of_REAL 2 st L1 _|_ L2 & C in L1 /\ L2 & A in L1 & B in L2 & A <> C & B <> C holds
A,B,C is_a_triangle
let L1, L2 be Element of line_of_REAL 2; :: thesis: ( L1 _|_ L2 & C in L1 /\ L2 & A in L1 & B in L2 & A <> C & B <> C implies A,B,C is_a_triangle )
assume that
A1: L1 _|_ L2 and
A2: C in L1 /\ L2 and
A3: A in L1 and
A4: B in L2 and
A5: A <> C and
A6: B <> C ; :: thesis: A,B,C is_a_triangle
not A in Line (B,C)

proof

assume A7: A in Line (B,C) ; :: thesis: contradiction
A8: ( C in L1 & C in L2 ) by A2, XBOOLE_0:def 4;
A9: ( L1 is being_line & L2 is being_line ) by A1, EUCLIDLP:67;
consider x being Element of REAL 2 such that
A10: L1 /\ L2 = {x} by A1, Th33;
A11: L1 /\ L2 = {C} by A2, A10, TARSKI:def 1;
( A in L2 & A in L1 ) by A3, A7, A4, A9, A8, A6, Th37;
then A in {C} by A11, XBOOLE_0:def 4;
hence contradiction by A5, TARSKI:def 1; :: thesis: verum

end;

hence A,B,C is_a_triangle by A6, MENELAUS:13; :: thesis: verum