theorem
:: JORDAN6:26
for
P
being
Subset
of
(
TOP-REAL
2
)
for
p1
,
p2
,
q1
,
q2
being
Point
of
(
TOP-REAL
2
)
holds
Segment
(
P
,
p1
,
p2
,
q1
,
q2
)
=
{
q
where
q
is
Point
of
(
TOP-REAL
2
)
: (
LE
q1
,
q
,
P
,
p1
,
p2
&
LE
q
,
q2
,
P
,
p1
,
p2
)
}