theorem
:: EUCLID12:51
for
A
,
B
,
C
being
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