let X, Y be non empty compact TopSpace; :: thesis: for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open holds
ex G being Subset-Family of [:Y,X:] st
( G c= F & G is Cover of [:Y,X:] & G is finite )
let F be Subset-Family of [:Y,X:]; :: thesis: ( F is Cover of [:Y,X:] & F is open implies ex G being Subset-Family of [:Y,X:] st
( G c= F & G is Cover of [:Y,X:] & G is finite ) )
assume A1: ( F is Cover of [:Y,X:] & F is open ) ; :: thesis: ex G being Subset-Family of [:Y,X:] st
( G c= F & G is Cover of [:Y,X:] & G is finite )
set R = { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ ) } ;
{ Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ ) } c= bool the carrier of X

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ ) } or s in bool the carrier of X )
assume s in { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ ) } ; :: thesis: s in bool the carrier of X
then consider Q1 being open Subset of X such that
A2: ( s = Q1 & ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q1:] c= union FQ ) ) ;
thus s in bool the carrier of X by A2; :: thesis: verum

end;

then reconsider R = { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ ) } as Subset-Family of X ;
reconsider R = R as Subset-Family of X ;
consider C being Subset-Family of X such that
A3: ( C c= R & C is finite & C is Cover of X ) by A1, Th22;
defpred S₁[ set , set ] means ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),$1:] c= union FQ & $2 = FQ );
A4: for e being set st e in C holds
ex u being set st S₁[e,u]

proof

let e be set ; :: thesis: ( e in C implies ex u being set st S₁[e,u] )
assume e in C ; :: thesis: ex u being set st S₁[e,u]
then e in R by A3;
then consider Q1 being open Subset of X such that
A5: ( Q1 = e & ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q1:] c= union FQ ) ) ;
thus ex u being set st S₁[e,u] by A5; :: thesis: verum

end;

consider t being Function such that
A6: ( dom t = C & ( for s being set st s in C holds
S₁[s,t . s] ) ) from CLASSES1:sch 1(A4);
A7: union (rng t) c= F

proof

let k be set ; :: according to TARSKI:def 3 :: thesis: ( not k in union (rng t) or k in F )
assume k in union (rng t) ; :: thesis: k in F
then consider K being set such that
A8: ( k in K & K in rng t ) by TARSKI:def 4;
consider x1 being set such that
A9: ( x1 in dom t & K = t . x1 ) by A8, FUNCT_1:def 5;
consider FQ being Subset-Family of [:Y,X:] such that
A10: ( FQ c= F & FQ is finite & [:([#] Y),x1:] c= union FQ & K = FQ ) by A6, A9;
thus k in F by A8, A10; :: thesis: verum

end;

A11: union (rng t) is finite

proof

A12: rng t is finite by A3, A6, FINSET_1:26;
for X1 being set st X1 in rng t holds
X1 is finite

proof

let X1 be set ; :: thesis: ( X1 in rng t implies X1 is finite )
assume X1 in rng t ; :: thesis: X1 is finite
then consider x1 being set such that
A13: ( x1 in dom t & X1 = t . x1 ) by FUNCT_1:def 5;
consider FQ being Subset-Family of [:Y,X:] such that
A14: ( FQ c= F & FQ is finite & [:([#] Y),x1:] c= union FQ & t . x1 = FQ ) by A6, A13;
thus X1 is finite by A13, A14; :: thesis: verum

end;

hence union (rng t) is finite by A12, FINSET_1:25; :: thesis: verum

end;

deffunc H₁( set ) -> set = [:([#] Y),$1:];
set CX = { H₁(f) where f is Subset of X : f in C } ;
{ H₁(f) where f is Subset of X : f in C } c= bool the carrier of [:Y,X:]

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in { H₁(f) where f is Subset of X : f in C } or s in bool the carrier of [:Y,X:] )
assume s in { H₁(f) where f is Subset of X : f in C } ; :: thesis: s in bool the carrier of [:Y,X:]
then consider f1 being Subset of X such that
A15: ( s = H₁(f1) & f1 in C ) ;
[:([#] Y),f1:] c= the carrier of [:Y,X:] ;
hence s in bool the carrier of [:Y,X:] by A15; :: thesis: verum

end;

then reconsider CX = { H₁(f) where f is Subset of X : f in C } as Subset-Family of [:Y,X:] ;
reconsider CX = CX as Subset-Family of [:Y,X:] ;
set G = union (rng t);
union (rng t) c= bool the carrier of [:Y,X:]

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in union (rng t) or s in bool the carrier of [:Y,X:] )
assume s in union (rng t) ; :: thesis: s in bool the carrier of [:Y,X:]
then s in F by A7;
hence s in bool the carrier of [:Y,X:] ; :: thesis: verum

end;

then reconsider G = union (rng t) as Subset-Family of [:Y,X:] ;
reconsider G = G as Subset-Family of [:Y,X:] ;
take G ; :: thesis: ( G c= F & G is Cover of [:Y,X:] & G is finite )
union CX = [:([#] Y),(union C):]

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: [:([#] Y),(union C):] c= union CX

let g be set ; :: thesis: ( g in union CX implies g in [:([#] Y),(union C):] )
assume g in union CX ; :: thesis: g in [:([#] Y),(union C):]
then consider GG being set such that
A16: ( g in GG & GG in CX ) by TARSKI:def 4;
consider FF being Subset of X such that
A17: ( GG = [:([#] Y),FF:] & FF in C ) by A16;
consider g1, g2 being set such that
A18: ( g1 in [#] Y & g2 in FF & g = [g1,g2] ) by A16, A17, ZFMISC_1:def 2;
g2 in union C by A17, A18, TARSKI:def 4;
hence g in [:([#] Y),(union C):] by A18, ZFMISC_1:106; :: thesis: verum

end;

let g be set ; :: according to TARSKI:def 3 :: thesis: ( not g in [:([#] Y),(union C):] or g in union CX )
assume g in [:([#] Y),(union C):] ; :: thesis: g in union CX
then consider g1, g2 being set such that
A19: ( g1 in [#] Y & g2 in union C & g = [g1,g2] ) by ZFMISC_1:def 2;
consider GG being set such that
A20: ( g2 in GG & GG in C ) by A19, TARSKI:def 4;
GG in { Q where Q is open Subset of X : ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ ) } by A3, A20;
then consider Q1 being open Subset of X such that
A21: ( GG = Q1 & ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q1:] c= union FQ ) ) ;
A22: g in [:([#] Y),Q1:] by A19, A20, A21, ZFMISC_1:106;
[:([#] Y),Q1:] in CX by A20, A21;
hence g in union CX by A22, TARSKI:def 4; :: thesis: verum

end;

then A23: union CX = [:([#] Y),([#] X):] by A3, SETFAM_1:60
.= [#] [:Y,X:] by BORSUK_1:def 5 ;
[#] [:Y,X:] c= union (union (rng t))

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in [#] [:Y,X:] or d in union (union (rng t)) )
assume d in [#] [:Y,X:] ; :: thesis: d in union (union (rng t))
then consider CC being set such that
A24: ( d in CC & CC in CX ) by A23, TARSKI:def 4;
consider Cc being Subset of X such that
A25: ( CC = [:([#] Y),Cc:] & Cc in C ) by A24;
Cc in R by A3, A25;
then consider Qq being open Subset of X such that
A26: ( Cc = Qq & ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Qq:] c= union FQ ) ) ;
consider d1, d2 being set such that
A27: ( d1 in [#] Y & d2 in Cc & d = [d1,d2] ) by A24, A25, ZFMISC_1:def 2;
consider FQ1 being Subset-Family of [:Y,X:] such that
A28: ( FQ1 c= F & FQ1 is finite & [:([#] Y),Qq:] c= union FQ1 & t . Qq = FQ1 ) by A6, A25, A26;
A29: FQ1 in rng t by A6, A25, A26, A28, FUNCT_1:def 5;
d in [:([#] Y),Qq:] by A26, A27, ZFMISC_1:106;
then consider DC being set such that
A30: ( d in DC & DC in FQ1 ) by A28, TARSKI:def 4;
DC in union (rng t) by A29, A30, TARSKI:def 4;
hence d in union (union (rng t)) by A30, TARSKI:def 4; :: thesis: verum

end;

then A31: union G = [#] [:Y,X:] by XBOOLE_0:def 10;
thus G c= F by A7; :: thesis: ( G is Cover of [:Y,X:] & G is finite )
thus G is Cover of [:Y,X:] by A31, SETFAM_1:def 12; :: thesis: G is finite
thus G is finite by A11; :: thesis: verum