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

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 set 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 by TOPS_2:def 2;
rngS is centered by A2, Th11;
then meet rngS <> {} by A1, A3, A4, Th21;
then consider x being set such that
A5: x in meet rngS by XBOOLE_0:def 1;

now

let n be Element of NAT ; :: thesis: x in S . n
dom S = NAT by FUNCT_2:def 1;
then S . n in rngS by FUNCT_1:def 3;
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 A6: for S being non-empty closed SetSequence of T st S is non-ascending holds
meet S <> {} ; :: thesis: T is countably_compact

now

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

now

per cases ( card F = omega or card F in omega ) by A10, 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
A11: dom s = NAT and
A12: rng s = F by WELLORD2:def 4;
reconsider s = s as SetSequence of T by A11, A12, FUNCT_2:2;
consider R being SetSequence of T such that
A13: R is non-ascending and
A14: ( F is centered implies R is non-empty ) and
( F is open implies R is open ) and
A15: ( F is closed implies R is closed ) and
A16: for i being natural number holds R . i = meet { (s . j) where j is Element of NAT : j <= i } by A12, Th13;
meet R <> {} by A6, A7, A8, A13, A14, A15;
then consider x being set such that
A17: x in meet R by XBOOLE_0:def 1;

A18: now

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

end;

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

end;

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

A24: F <> {} by A7, FINSET_1:def 3;
F is finite by A23;
hence not meet F is empty by A7, A24, FINSET_1:def 3; :: thesis: verum

end;

end;

end;

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

end;

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