let A, B, C be Point of (TOP-REAL 2); 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; ( 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
; A,B,C is_a_triangle
not A in Line (B,C)
proof
assume A7:
A in Line (
B,
C)
;
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;
verum
end;
hence
A,B,C is_a_triangle
by A6, MENELAUS:13; verum