let T be non empty TopSpace; :: thesis: ( T is countably_compact implies for F being Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds
F is finite )
assume A1: T is countably_compact ; :: thesis: for F being Subset-Family of T st F is locally_finite & F is with_non-empty_elements holds
F is finite
given F being Subset-Family of T such that A2: F is locally_finite and
A3: F is with_non-empty_elements and
A4: F is infinite ; :: thesis: contradiction
consider f being sequence of F such that
A5: f is one-to-one by A4, DICKSON:3;
A6: rng f c= F ;
reconsider f = f as SetSequence of T by A4, FUNCT_2:7;

now :: thesis: for x being object st x in dom f holds
not f . x is empty

let x be object ; :: thesis: ( x in dom f implies not f . x is empty )
assume x in dom f ; :: thesis: not f . x is empty
then f . x in rng f by FUNCT_1:def 3;
hence not f . x is empty by A3, A6; :: thesis: verum

end;

then f is non-empty by FUNCT_1:def 9;
then ex R being non-empty closed SetSequence of T st
( R is non-ascending & ( F is locally_finite & f is one-to-one implies meet R = {} ) & ( for i being Nat ex fi being Subset-Family of T st
( R . i = Cl (union fi) & fi = { (f . j) where j is Element of NAT : j >= i } ) ) ) by A6, Th23;
hence contradiction by A1, A2, A5, Th22; :: thesis: verum