let
S
be
compact
Subset
of
(
TOP-REAL
2
)
;
:: thesis:
proj2
.:
S
is
compact
proj2
.:
S
is
closed
by
Th13
;
hence
proj2
.:
S
is
compact
by
Th14
,
RCOMP_1:11
;
:: thesis:
verum