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 ) )
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 object ; :: 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 ex Q1 being open Subset of X st
( s = Q1 & ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q1:] c= union FQ ) ) ;
hence s in bool the carrier of X ; :: 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 ;
defpred S₁[ object , object ] means ex D1 being set ex FQ being Subset-Family of [:Y,X:] st
( D1 = $1 & FQ c= F & FQ is finite & [:([#] Y),D1:] c= union FQ & $2 = FQ );
deffunc H₁( set ) -> set = [:([#] Y),$1:];
assume ( 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 )
then consider C being Subset-Family of X such that
A1: C c= R and
A2: C is finite and
A3: C is Cover of X by Th19;
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 object ; :: 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
A4: s = H₁(f1) and
f1 in C ;
[:([#] Y),f1:] c= the carrier of [:Y,X:] ;
hence s in bool the carrier of [:Y,X:] by A4; :: 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:] ;
A5: for e being object st e in C holds
ex u being object st S₁[e,u]

proof

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

end;

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

proof

let k be object ; :: 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 and
A9: K in rng t by TARSKI:def 4;
consider x1 being object such that
A10: ( x1 in dom t & K = t . x1 ) by A9, FUNCT_1:def 3;
reconsider x1 = x1 as set by TARSKI:1;
S₁[x1,t . x1] by A6, A10;
then ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),x1:] c= union FQ & K = FQ ) by A10;
hence k in F by A8; :: thesis: verum

end;

union (rng t) c= bool the carrier of [:Y,X:]

proof

let s be object ; :: 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 )
thus G c= F by A7; :: thesis: ( 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 object ; :: 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
A11: g in GG and
A12: GG in CX by TARSKI:def 4;
consider FF being Subset of X such that
A13: GG = [:([#] Y),FF:] and
A14: FF in C by A12;
consider g1, g2 being object such that
A15: g1 in [#] Y and
A16: g2 in FF and
A17: g = [g1,g2] by A11, A13, ZFMISC_1:def 2;
g2 in union C by A14, A16, TARSKI:def 4;
hence g in [:([#] Y),(union C):] by A15, A17, ZFMISC_1:87; :: thesis: verum

end;

let g be object ; :: 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 object such that
A18: g1 in [#] Y and
A19: g2 in union C and
A20: g = [g1,g2] by ZFMISC_1:def 2;
consider GG being set such that
A21: g2 in GG and
A22: 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 A1, A22;
then consider Q1 being open Subset of X such that
A23: GG = Q1 and
ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q1:] c= union FQ ) ;
A24: [:([#] Y),Q1:] in CX by A22, A23;
g in [:([#] Y),Q1:] by A18, A20, A21, A23, ZFMISC_1:87;
hence g in union CX by A24, TARSKI:def 4; :: thesis: verum

end;

then A25: union CX = [:([#] Y),([#] X):] by A3, SETFAM_1:45
.= [#] [:Y,X:] by BORSUK_1:def 2 ;
[#] [:Y,X:] c= union (union (rng t))

proof

let d be object ; :: 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
A26: d in CC and
A27: CC in CX by A25, TARSKI:def 4;
consider Cc being Subset of X such that
A28: CC = [:([#] Y),Cc:] and
A29: Cc in C by A27;
Cc in R by A1, A29;
then consider Qq being open Subset of X such that
A30: Cc = Qq and
ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Qq:] c= union FQ ) ;
S₁[Cc,t . Cc] by A6, A29;
then consider FQ1 being Subset-Family of [:Y,X:] such that
FQ1 c= F and
FQ1 is finite and
A31: [:([#] Y),Qq:] c= union FQ1 and
A32: t . Qq = FQ1 by A30;
consider DC being set such that
A33: d in DC and
A34: DC in FQ1 by A26, A28, A30, A31, TARSKI:def 4;
FQ1 in rng t by A6, A29, A30, A32, FUNCT_1:def 3;
then DC in union (rng t) by A34, TARSKI:def 4;
hence d in union (union (rng t)) by A33, TARSKI:def 4; :: thesis: verum

end;

hence G is Cover of [:Y,X:] by SETFAM_1:def 11; :: thesis: G is finite
A35: 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 object such that
A36: x1 in dom t and
A37: X1 = t . x1 by FUNCT_1:def 3;
reconsider x1 = x1 as set by TARSKI:1;
S₁[x1,t . x1] by A6, A36;
then ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),x1:] c= union FQ & t . x1 = FQ ) ;
hence X1 is finite by A37; :: thesis: verum

end;

rng t is finite by A2, A6, FINSET_1:8;
hence G is finite by A35, FINSET_1:7; :: thesis: verum