reconsider B = {x} as Subset of X ;

_{1} being Subset of X st b_{1} = {x} holds

b_{1} is compact
by COMPTS_1:def 4; :: thesis: verum

now :: thesis: for F being Subset-Family of X st F is Cover of B & F is open holds

ex G being Subset-Family of X st

( G c= F & G is Cover of B & G is finite )

hence
for bex G being Subset-Family of X st

( G c= F & G is Cover of B & G is finite )

let F be Subset-Family of X; :: thesis: ( F is Cover of B & F is open implies ex G being Subset-Family of X st

( G c= F & G is Cover of B & G is finite ) )

assume that

A1: F is Cover of B and

F is open ; :: thesis: ex G being Subset-Family of X st

( G c= F & G is Cover of B & G is finite )

B c= union F by A1, SETFAM_1:def 11;

then x in union F by ZFMISC_1:31;

then consider A being set such that

A2: x in A and

A3: A in F by TARSKI:def 4;

reconsider G = {A} as Subset-Family of X by A3, ZFMISC_1:31;

take G = G; :: thesis: ( G c= F & G is Cover of B & G is finite )

thus G c= F by A3, ZFMISC_1:31; :: thesis: ( G is Cover of B & G is finite )

x in union G by A2;

then B c= union G by ZFMISC_1:31;

hence G is Cover of B by SETFAM_1:def 11; :: thesis: G is finite

thus G is finite ; :: thesis: verum

end;( G c= F & G is Cover of B & G is finite ) )

assume that

A1: F is Cover of B and

F is open ; :: thesis: ex G being Subset-Family of X st

( G c= F & G is Cover of B & G is finite )

B c= union F by A1, SETFAM_1:def 11;

then x in union F by ZFMISC_1:31;

then consider A being set such that

A2: x in A and

A3: A in F by TARSKI:def 4;

reconsider G = {A} as Subset-Family of X by A3, ZFMISC_1:31;

take G = G; :: thesis: ( G c= F & G is Cover of B & G is finite )

thus G c= F by A3, ZFMISC_1:31; :: thesis: ( G is Cover of B & G is finite )

x in union G by A2;

then B c= union G by ZFMISC_1:31;

hence G is Cover of B by SETFAM_1:def 11; :: thesis: G is finite

thus G is finite ; :: thesis: verum

b