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

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