reconsider B = {x} as Subset of X ;
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 )
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;
hence for b1 being Subset of X st b1 = {x} holds
b1 is compact by COMPTS_1:def 4; :: thesis: verum