let T be non empty T_1 TopSpace; :: thesis: ( ( for A being Subset of T st not A is finite & A is countable holds
not Der A is empty ) implies T is countably_compact )
assume A1: for A being Subset of T st not A is finite & A is countable holds
not Der A is empty ; :: 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);
reconsider rngF = rng F as Subset of T ;

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;

dom F = NAT by FUNCT_2:def 1;
then rng F is countable by CARD_3:127;
then not Der rngF is empty by A1, B7, A2, Th25;
then consider p being set such that
A8: p in Der rngF by XBOOLE_0:def 1;
reconsider p = p as Point of T by A8;
consider n being Element of NAT such that
A9: not p in S . n by A2, KURATO_2:6;
deffunc H₁( set ) -> set = F . $1;
set F1n = { H₁(i) where i is Element of NAT : i in n + 1 } ;
A10: n + 1 is finite ;
A11: { H₁(i) where i is Element of NAT : i in n + 1 } is finite from FRAENKEL:sch 21(A10);
{ H₁(i) where i is Element of NAT : i in n + 1 } c= the carrier of T

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₁(i) where i is Element of NAT : i in n + 1 } or x in the carrier of T )
assume A12: x in { H₁(i) where i is Element of NAT : i in n + 1 } ; :: thesis: x in the carrier of T
ex i being Element of NAT st
( x = F . i & i in n + 1 ) by A12;
hence x in the carrier of T ; :: thesis: verum

end;

then reconsider F1n = { H₁(i) where i is Element of NAT : i in n + 1 } as Subset of T ;
set U = ((S . n) ` ) \ (F1n \ {p});
reconsider U = ((S . n) ` ) \ (F1n \ {p}) as Subset of T ;
( F1n \ {p} is finite & S . n is closed ) by A11, Def6;
then A13: U is open by FRECHET:4;
p in {p} by TARSKI:def 1;
then ( not p in F1n \ {p} & p in (S . n) ` ) by A9, XBOOLE_0:def 5;
then p in U by XBOOLE_0:def 5;
then consider q being Point of T such that
A14: ( q in rngF /\ U & q <> p ) by A8, A13, TOPGEN_1:19;
q in rngF by A14, XBOOLE_0:def 4;
then consider i being set such that
A15: ( i in dom F & F . i = q ) by FUNCT_1:def 5;
reconsider i = i as Element of NAT by A15;

per cases ( i <= n or i > n ) ;

suppose i <= n ; :: thesis: contradiction

then i < n + 1 by NAT_1:13;
then i in n + 1 by NAT_1:45;
then q in F1n by A15;
then q in F1n \ {p} by A14, ZFMISC_1:64;
then not q in U by XBOOLE_0:def 5;
hence contradiction by A14, XBOOLE_0:def 4; :: thesis: verum

end;

suppose i > n ; :: thesis: contradiction

then ( q in S . i & S . i c= S . n ) by A2, A6, A15, PROB_1:def 6;
then not q in (S . n) ` by XBOOLE_0:def 5;
then not q in U by XBOOLE_0:def 5;
hence contradiction by A14, XBOOLE_0:def 4; :: thesis: verum

end;

end;