reconsider C = {} as Subset-Family of T by XBOOLE_1:2;
let S be Subset of T; :: thesis: ( S is empty implies S is compact )
assume S is empty ; :: thesis: S is compact
then A1: S c= union C ;
let F be Subset-Family of T; :: according to COMPTS_1:def 4 :: thesis: ( F is Cover of S & F is open implies ex G being Subset-Family of T st
( G c= F & G is Cover of S & G is finite ) )
assume that
F is Cover of S and
F is open ; :: thesis: ex G being Subset-Family of T st
( G c= F & G is Cover of S & G is finite )
take C ; :: thesis: ( C c= F & C is Cover of S & C is finite )
thus ( C c= F & C is Cover of S & C is finite ) by A1, SETFAM_1:def 11; :: thesis: verum