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

proof

assume A1: T is countably_compact ; :: thesis: for S being non-empty closed SetSequence of T st S is non-ascending holds
meet S <> {}
let S be non-empty closed SetSequence of T; :: thesis: ( S is non-ascending implies meet S <> {} )
assume A2: S is non-ascending ; :: thesis: meet S <> {}
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: for D being Subset of T st D in rngS holds
D is closed

let D be Subset of T; :: thesis: ( D in rngS implies D is closed )
assume D in rngS ; :: thesis: D is closed
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: verum

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: for n being Nat holds x in S . n

let n be Nat; :: thesis: x in S . n
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: verum

end;

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

end;

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

now :: thesis: for F being Subset-Family of T st F is centered & F is closed & F is countable holds
meet F <> {}

let F be Subset-Family of T; :: thesis: ( F is centered & F is closed & F is countable implies meet F <> {} )
assume that
A8: F is centered and
A9: F is closed and
A10: F is countable ; :: thesis: meet F <> {}
A11: card F c= omega by A10, CARD_3:def 14;

now :: thesis: not meet F is empty

per cases ( card F = omega or card F in omega ) by A11, CARD_1:3;

suppose card F = omega ; :: thesis: not meet F is empty

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 non-ascending 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: for y being set st y in F holds
x in y

let y be set ; :: thesis: ( y in F implies x in y )
assume y in F ; :: thesis: x in y
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: verum

end;

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

end;

suppose A24: card F in omega ; :: thesis: not meet F is empty

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

end;

end;

end;

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

end;

hence T is countably_compact by Th21; :: thesis: verum