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