theorem
Th4
:
:: JORDAN6:4
for
r
being
Real
for
P
being
Subset
of
(
TOP-REAL
2
)
st
P
=
{
p
where
p
is
Point
of
(
TOP-REAL
2
)
:
p
`1
>=
r
}
holds
P
is
closed