theorem
Th14
:
:: JORDAN6:14
for
P
,
Q
being
Subset
of
(
TOP-REAL
2
)
for
p1
,
p2
being
Point
of
(
TOP-REAL
2
)
st
P
is_an_arc_of
p1
,
p2
&
Q
=
{
q
where
q
is
Point
of
(
TOP-REAL
2
)
:
q
`2
=
(
(
p1
`2
)
+
(
p2
`2
)
)
/
2
}
holds
(
P
meets
Q
&
P
/\
Q
is
closed
)