deffunc H₁( set ) -> set = meet $1;
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 and
A3: meet S = {} by Th22;
defpred S₁[ object , object ] means $2 in S . $1;
A4: for x being object st x in NAT holds
ex y being object st
( y in the carrier of T & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in the carrier of T & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being object st
( y in the carrier of T & S₁[x,y] )
then reconsider x9 = x as Element of NAT ;
dom S = NAT by FUNCT_2:def 1;
then not S . x9 is empty by FUNCT_1:def 9;
then consider y being object such that
A5: y in S . x9 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 object st x in NAT holds
S₁[x,F . x] from FUNCT_2:sch 1(A4);
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;
A7: A is locally_finite

proof

deffunc H₂( set ) -> set = {(F . $1)};
let x be Point of T; :: according to PCOMPS_1:def 1 :: 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 Nat such that
A8: not x in S . i by A3, KURATO_0:3;
take Si9 = (S . i) ` ; :: thesis: ( x in Si9 & Si9 is open & { b₁ where b₁ is Element of bool the carrier of T : ( b₁ in A & not b₁ misses Si9 ) } is finite )
S . i is closed by Def6;
hence ( x in Si9 & Si9 is open ) by A8, SUBSET_1:29; :: thesis: { b₁ where b₁ is Element of bool the carrier of T : ( b₁ in A & not b₁ misses Si9 ) } is finite
set meetS = { V where V is Subset of T : ( V in A & V meets Si9 ) } ;
set SI = { H₂(j) where j is Element of NAT : j in i } ;
A9: { V where V is Subset of T : ( V in A & V meets Si9 ) } c= { H₂(j) where j is Element of NAT : j in i }

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in { V where V is Subset of T : ( V in A & V meets Si9 ) } or v in { H₂(j) where j is Element of NAT : j in i } )
assume v in { V where V is Subset of T : ( V in A & V meets Si9 ) } ; :: thesis: v in { H₂(j) where j is Element of NAT : j in i }
then consider V being Subset of T such that
A10: V = v and
A11: V in A and
A12: V meets Si9 ;
consider y being Point of T such that
A13: V = {y} and
A14: y in rng F by A11;
consider z being object such that
A15: z in dom F and
A16: y = F . z by A14, FUNCT_1:def 3;
reconsider z = z as Element of NAT by A15;
z in Segm i

proof

assume not z in Segm i ; :: thesis: contradiction
then z >= i by NAT_1:44;
then A17: S . z c= S . i by A2, PROB_1:def 4;
A18: y in Si9 by A12, A13, ZFMISC_1:50;
y in S . z by A6, A16;
hence contradiction by A17, A18, XBOOLE_0:def 5; :: thesis: verum

end;

hence v in { H₂(j) where j is Element of NAT : j in i } by A10, A13, A16; :: thesis: verum

end;

A19: i is finite ;
{ H₂(j) where j is Element of NAT : j in i } is finite from FRAENKEL:sch 21(A19);
hence { b₁ where b₁ is Element of bool the carrier of T : ( b₁ in A & not b₁ misses Si9 ) } is finite by A9; :: thesis: verum

end;

set PP = { H₁(y) where y is Element of bool the carrier of T : y in A } ;
A20: rngF c= { H₁(y) where y is Element of bool the carrier of T : y in A }

proof

let y be object ; :: 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 A21: y in rngF ; :: thesis: y in { H₁(y) where y is Element of bool the carrier of T : y in A }
reconsider y9 = y as Point of T by A21;
{y9} in A by A21;
then H₁({y9}) 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:10; :: thesis: verum

end;

A22: for n being Nat holds F . n in S . n by A6, ORDINAL1:def 12;

now :: thesis: for a being Subset of T st a in A holds
card a = 1

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

end;

then A23: A is finite by A1, A7;
{ H₁(y) where y is Element of bool the carrier of T : y in A } is finite from FRAENKEL:sch 21(A23);
hence contradiction by A2, A3, A22, A20, Th24; :: thesis: verum