let
S
be
closed
Subset
of
(
TOP-REAL
2
)
;
:: thesis:
(
S
is
bounded
implies
proj2
.:
S
is
closed
)
assume
S
is
bounded
;
:: thesis:
proj2
.:
S
is
closed
then
Cl
(
proj2
.:
S
)
=
proj2
.:
(
Cl
S
)
by
TOPREAL6:84
.=
proj2
.:
S
by
PRE_TOPC:22
;
hence
proj2
.:
S
is
closed
;
:: thesis:
verum