let T be non empty T_1 TopSpace; :: thesis: ( ( for A being Subset of T st A is infinite & A is countable holds
not Der A is empty ) implies T is countably_compact )
assume A1: for A being Subset of T st A is infinite & 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 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 ;
A7: for n being Nat holds F . n in S . n by A6, ORDINAL1:def 12;
dom F = NAT by FUNCT_2:def 1;
then rng F is countable by CARD_3:93;
then not Der rngF is empty by A1, A2, A3, A7, Th24;
then consider p being object such that
A8: p in Der rngF by XBOOLE_0:def 1;
reconsider p = p as Point of T by A8;
consider n being Nat such that
A9: not p in S . n by A3, KURATO_0:3;
A10: p in (S . n) ` by A9, XBOOLE_0:def 5;
deffunc H₁( set ) -> set = F . $1;
set F1n = { H₁(i) where i is Element of NAT : i in n + 1 } ;
A11: { H₁(i) where i is Element of NAT : i in n + 1 } c= the carrier of T

proof

let x be object ; :: 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 x in { H₁(i) where i is Element of NAT : i in n + 1 } ; :: thesis: x in the carrier of T
then ex i being Element of NAT st
( x = F . i & i in n + 1 ) ;
hence x in the carrier of T ; :: thesis: verum

end;

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

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

suppose i <= n ; :: thesis: contradiction

then i < n + 1 by NAT_1:13;
then i in Segm (n + 1) by NAT_1:44;
then q in F1n by A18;
then q in F1n \ {p} by A16, ZFMISC_1:56;
then not q in U by XBOOLE_0:def 5;
hence contradiction by A15, XBOOLE_0:def 4; :: thesis: verum

end;

suppose i > n ; :: thesis: contradiction

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

end;

end;