deffunc H₁( set ) -> set = meet $1;
let T be non empty TopSpace; :: thesis: ( ( for F being Subset-Family of st F is locally_finite & ( for A being Subset of 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 st F is locally_finite & ( for A being Subset of 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 such that
A2: S is non-ascending and
A3: meet S = {} by Th22;
defpred S₁[ set , set ] means $2 in S . $1;
A4: 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 x in NAT ; :: thesis: ex y being set st
( y in the carrier of T & S₁[x,y] )
then reconsider x' = x as Element of NAT ;
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(A4);
reconsider rngF = rng F as Subset of ;
set A = { {x} where x is Element of : x in rngF } ;
reconsider A = { {x} where x is Element of : x in rngF } as Subset-Family of by RELSET_2:16;
A7: A is locally_finite

proof

deffunc H₂( set ) -> set = {(F . $1)};
let x be Point of ; :: 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
A8: not x in S . i by A3, 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 A8, SUBSET_1:50; :: thesis: { b₁ where b₁ is Element of bool the carrier of T : ( b₁ in A & not b₁ misses Si' ) } is finite
set meetS = { V where V is Subset of : ( V in A & V meets Si' ) } ;
set SI = { H₂(j) where j is Element of NAT : j in i } ;
A9: { V where V is Subset of : ( 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 : ( V in A & V meets Si' ) } or v in { H₂(j) where j is Element of NAT : j in i } )
assume v in { V where V is Subset of : ( V in A & V meets Si' ) } ; :: thesis: v in { H₂(j) where j is Element of NAT : j in i }
then consider V being Subset of such that
A10: V = v and
A11: V in A and
A12: V meets Si' ;
consider y being Point of such that
A13: V = {y} and
A14: y in rng F by A11;
consider z being set such that
A15: z in dom F and
A16: 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 A17: S . z c= S . i by A2, PROB_1:def 6;
A18: y in Si' by A12, A13, ZFMISC_1:56;
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 Si' ) } 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 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 A21: 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 by A21;
{y'} in A by A21;
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;

A22: 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;

now

let a be Subset of ; :: thesis: ( a in A implies card a = 1 )
assume a in A ; :: thesis: card a = 1
then ex y being Point of st
( a = {y} & y in rngF ) ;
hence card a = 1 by CARD_1:50; :: 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, Th25; :: thesis: verum