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)

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

hence
A,B,C is_a_triangle
by A6, MENELAUS:13; :: thesis: verum
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;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