theorem
Th11
:
:: EUCLID12:13
for
A
,
B
,
C
being
Point
of
(
TOP-REAL
2
)
for
p
,
q
,
r
being
Element
of
(
Euclid
2
)
st
p
,
q
,
r
are_mutually_distinct
&
p
=
A
&
q
=
B
&
r
=
C
holds
(
A
in
LSeg
(
B
,
C
) iff
p
is_between
q
,
r
)