let
A
be
Subset
of
T
;
:: thesis:
(
A
is
finite
implies
A
is
compact
)
assume
A
is
finite
;
:: thesis:
A
is
compact
then
reconsider
B
=
A
as
finite
Subset
of
T
;
[#]
(
T

B
)
=
B
by
PRE_TOPC:def 5
;
then
A1
:
T

B
is
compact
;
(
B
=
{}
or
B
<>
{}
) ;
hence
A
is
compact
by
A1
,
Th3
;
:: thesis:
verum