let T be non empty TopSpace; :: thesis: ( ( for F being Subset-Family of T st F is locally_finite & ( for A being Subset of T st A in F holds
card A = 1 ) holds
F is finite ) implies T is countably_compact )
assume A1: for F being Subset-Family of T st F is locally_finite & ( for A being Subset of T st A in F holds
card A = 1 ) holds
F is finite ; :: thesis: T is countably_compact
assume not T is countably_compact ; :: thesis: contradiction
then consider S being non-empty closed SetSequence of T such that
A2: ( S is non-ascending & meet S = {} ) by Th22;
defpred S₁[ set , set ] means $2 in S . $1;
A3: for x being set st x in NAT holds
ex y being set st
( y in the carrier of T & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in the carrier of T & S₁[x,y] ) )
assume A4: x in NAT ; :: thesis: ex y being set st
( y in the carrier of T & S₁[x,y] )
reconsider x' = x as Element of NAT by A4;
dom S = NAT by FUNCT_2:def 1;
then not S . x' is empty by FUNCT_1:def 15;
then consider y being set such that
A5: y in S . x' by XBOOLE_0:def 1;
take y ; :: thesis: ( y in the carrier of T & S₁[x,y] )
thus ( y in the carrier of T & S₁[x,y] ) by A5; :: thesis: verum

end;

consider F being sequence of T such that
A6: for x being set st x in NAT holds
S₁[x,F . x] from FUNCT_2:sch 1(A3);

B7: now

let n be natural number ; :: thesis: F . n in S . n
n in NAT by ORDINAL1:def 13;
hence F . n in S . n by A6; :: thesis: verum

end;

reconsider rngF = rng F as Subset of T ;
set A = { {x} where x is Element of T : x in rngF } ;
reconsider A = { {x} where x is Element of T : x in rngF } as Subset-Family of T by RELSET_2:16;
A8: A is locally_finite

proof

let x be Point of T; :: according to PCOMPS_1:def 2 :: thesis: ex b₁ being Element of bool the carrier of T st
( x in b₁ & b₁ is open & { b₂ where b₂ is Element of bool the carrier of T : ( b₂ in A & not b₂ misses b₁ ) } is finite )
consider i being Element of NAT such that
A9: not x in S . i by A2, KURATO_2:6;
take Si' = (S . i) ` ; :: thesis: ( x in Si' & Si' is open & { b₁ where b₁ is Element of bool the carrier of T : ( b₁ in A & not b₁ misses Si' ) } is finite )
S . i is closed by Def6;
hence ( x in Si' & Si' is open ) by A9, SUBSET_1:50; :: thesis: { b₁ where b₁ is Element of bool the carrier of T : ( b₁ in A & not b₁ misses Si' ) } is finite
deffunc H₁( set ) -> set = {(F . $1)};
A10: i is finite ;
set SI = { H₁(j) where j is Element of NAT : j in i } ;
A11: { H₁(j) where j is Element of NAT : j in i } is finite from FRAENKEL:sch 21(A10);
set meetS = { V where V is Subset of T : ( V in A & V meets Si' ) } ;
{ V where V is Subset of T : ( V in A & V meets Si' ) } c= { H₁(j) where j is Element of NAT : j in i }

proof

let v be set ; :: according to TARSKI:def 3 :: thesis: ( not v in { V where V is Subset of T : ( V in A & V meets Si' ) } or v in { H₁(j) where j is Element of NAT : j in i } )
assume A12: v in { V where V is Subset of T : ( V in A & V meets Si' ) } ; :: thesis: v in { H₁(j) where j is Element of NAT : j in i }
consider V being Subset of T such that
A13: ( V = v & V in A & V meets Si' ) by A12;
consider y being Point of T such that
A14: ( V = {y} & y in rng F ) by A13;
consider z being set such that
A15: ( z in dom F & y = F . z ) by A14, FUNCT_1:def 5;
reconsider z = z as Element of NAT by A15;
z in i

proof

assume not z in i ; :: thesis: contradiction
then z >= i by NAT_1:45;
then ( y in S . z & S . z c= S . i ) by A2, A6, A15, PROB_1:def 6;
then ( y in S . i & y in Si' ) by A13, A14, ZFMISC_1:56;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum

end;

hence v in { H₁(j) where j is Element of NAT : j in i } by A13, A14, A15; :: thesis: verum

end;

hence { b₁ where b₁ is Element of bool the carrier of T : ( b₁ in A & not b₁ misses Si' ) } is finite by A11; :: thesis: verum

end;

now

let a be Subset of T; :: thesis: ( a in A implies card a = 1 )
assume A16: a in A ; :: thesis: card a = 1
ex y being Point of T st
( a = {y} & y in rngF ) by A16;
hence card a = 1 by CARD_1:50; :: thesis: verum

end;

then A17: A is finite by A1, A8;
deffunc H₁( set ) -> set = meet $1;
set PP = { H₁(y) where y is Element of bool the carrier of T : y in A } ;
A18: { H₁(y) where y is Element of bool the carrier of T : y in A } is finite from FRAENKEL:sch 21(A17);
rngF c= { H₁(y) where y is Element of bool the carrier of T : y in A }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rngF or y in { H₁(y) where y is Element of bool the carrier of T : y in A } )
assume A19: y in rngF ; :: thesis: y in { H₁(y) where y is Element of bool the carrier of T : y in A }
reconsider y' = y as Point of T by A19;
( {y'} in A & {y'} is Subset of T ) by A19;
then H₁({y'}) in { H₁(y) where y is Element of bool the carrier of T : y in A } ;
hence y in { H₁(y) where y is Element of bool the carrier of T : y in A } by SETFAM_1:11; :: thesis: verum

end;

hence contradiction by B7, A18, A2, Th25; :: thesis: verum