let T be non empty TopSpace; :: thesis:
thus ( T is countably_compact implies for S being non-empty closed SetSequence of T st S is V176() holds
meet S <> {} ) :: thesis:

proof

assume A1: T is countably_compact ; :: thesis:
let S be non-empty closed SetSequence of T; :: thesis:
assume A2: S is V176() ; :: thesis:
reconsider rngS = rng S as Subset-Family of T ;
dom S = NAT by FUNCT_2:def 1;
then A3: rngS is countable by CARD_3:93;

now :: thesis:

let D be Subset of T; :: thesis:
assume D in rngS ; :: thesis:
then ex x being object st
( x in dom S & S . x = D ) by FUNCT_1:def 3;
hence D is closed by Def6; :: thesis:

end;

then A4: rngS is closed ;
rngS is centered by A2, Th11;
then meet rngS <> {} by A1, A3, A4, Th21;
then consider x being object such that
A5: x in meet rngS by XBOOLE_0:def 1;

now :: thesis:

let n be Nat; :: thesis:
A6: n in NAT by ORDINAL1:def 12;
dom S = NAT by FUNCT_2:def 1;
then S . n in rngS by FUNCT_1:def 3, A6;
hence x in S . n by A5, SETFAM_1:def 1; :: thesis:

end;

hence meet S <> {} by KURATO_0:3; :: thesis:

end;

assume A7: for S being non-empty closed SetSequence of T st S is V176() holds
meet S <> {} ; :: thesis:

now :: thesis:

let F be Subset-Family of T; :: thesis:
assume that
A8: F is centered and
A9: F is closed and
A10: F is countable ; :: thesis:
A11: card F c= omega by A10, CARD_3:def 14;

now :: thesis:

per cases by A11, CARD_1:3;

suppose card F = omega ; :: thesis:

then NAT ,F are_equipotent by CARD_1:5, CARD_1:47;
then consider s being Function such that
s is one-to-one and
A12: dom s = NAT and
A13: rng s = F by WELLORD2:def 4;
reconsider s = s as SetSequence of T by A12, A13, FUNCT_2:2;
consider R being SetSequence of T such that
A14: R is V176() and
A15: ( F is centered implies R is non-empty ) and
( F is open implies R is open ) and
A16: ( F is closed implies R is closed ) and
A17: for i being Nat holds R . i = meet { (s . j) where j is Element of NAT : j <= i } by A13, Th13;
meet R <> {} by A7, A8, A9, A14, A15, A16;
then consider x being object such that
A18: x in meet R by XBOOLE_0:def 1;

A19: now :: thesis:

let y be set ; :: thesis:
assume y in F ; :: thesis:
then consider z being object such that
A20: z in dom s and
A21: s . z = y by A13, FUNCT_1:def 3;
reconsider z = z as Element of NAT by A20;
A22: s . z in { (s . j) where j is Element of NAT : j <= z } ;
A23: x in R . z by A18, KURATO_0:3;
R . z = meet { (s . j) where j is Element of NAT : j <= z } by A17;
then R . z c= s . z by A22, SETFAM_1:3;
hence x in y by A21, A23; :: thesis:

end;

not F is empty by A12, A13, RELAT_1:42;
hence not meet F is empty by A19, SETFAM_1:def 1; :: thesis:

end;

suppose A24: card F in omega ; :: thesis:

F is finite by A24;
hence not meet F is empty by A8, FINSET_1:def 3; :: thesis:

end;

end;

end;

hence meet F <> {} ; :: thesis:

end;

hence T is countably_compact by Th21; :: thesis: