let X, Y be non empty compact TopSpace; :: thesis: for R being Subset-Family of X
for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open & 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 ) } holds
( R is open & R is Cover of X )
let R be Subset-Family of X; :: thesis: for F being Subset-Family of [:Y,X:] st F is Cover of [:Y,X:] & F is open & 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 ) } holds
( R is open & R is Cover of X )
let F be Subset-Family of [:Y,X:]; :: thesis: ( F is Cover of [:Y,X:] & F is open & 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 ) } implies ( R is open & R is Cover of X ) )
assume that
A1: F is Cover of [:Y,X:] and
A2: F is open and
A3: 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 ) } ; :: thesis: ( R is open & R is Cover of X )

now :: thesis: for P being Subset of X st P in R holds
P is open

let P be Subset of X; :: thesis: ( P in R implies P is open )
assume P in R ; :: thesis: P is open
then ex E being open Subset of X st
( E = P & ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),E:] c= union FQ ) ) by A3;
hence P is open ; :: thesis: verum

end;

hence R is open ; :: thesis: R is Cover of X
A4: union F = [#] [:Y,X:] by A1, SETFAM_1:45;
[#] X c= union R

proof

let k be object ; :: according to TARSKI:def 3 :: thesis: ( not k in [#] X or k in union R )
assume k in [#] X ; :: thesis: k in union R
then reconsider k9 = k as Point of X ;
reconsider Z = [:([#] Y),{k9}:] as Subset of [:Y,X:] ;
( F is Cover of Z & Z is compact ) by A4, Th16, SETFAM_1:def 11;
then consider G being Subset-Family of [:Y,X:] such that
A5: G c= F and
A6: G is Cover of Z and
A7: G is finite by A2;
set uR = union G;
set Q = { x where x is Point of X : [:([#] Y),{x}:] c= union G } ;
{ x where x is Point of X : [:([#] Y),{x}:] c= union G } c= the carrier of X

proof

let k be object ; :: according to TARSKI:def 3 :: thesis: ( not k in { x where x is Point of X : [:([#] Y),{x}:] c= union G } or k in the carrier of X )
assume k in { x where x is Point of X : [:([#] Y),{x}:] c= union G } ; :: thesis: k in the carrier of X
then ex x1 being Point of X st
( k = x1 & [:([#] Y),{x1}:] c= union G ) ;
hence k in the carrier of X ; :: thesis: verum

end;

then reconsider Q = { x where x is Point of X : [:([#] Y),{x}:] c= union G } as Subset of X ;
Z c= union G by A6, SETFAM_1:def 11;
then A8: k9 in Q ;
A9: ex FQ being Subset-Family of [:Y,X:] st
( FQ c= F & FQ is finite & [:([#] Y),Q:] c= union FQ )

proof

take G ; :: thesis: ( G c= F & G is finite & [:([#] Y),Q:] c= union G )
[:([#] Y),Q:] c= union G

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in [:([#] Y),Q:] or z in union G )
assume z in [:([#] Y),Q:] ; :: thesis: z in union G
then consider x1, x2 being object such that
A10: x1 in [#] Y and
A11: x2 in Q and
A12: z = [x1,x2] by ZFMISC_1:def 2;
consider x29 being Point of X such that
A13: x29 = x2 and
A14: [:([#] Y),{x29}:] c= union G by A11;
x2 in {x29} by A13, TARSKI:def 1;
then z in [:([#] Y),{x29}:] by A10, A12, ZFMISC_1:87;
hence z in union G by A14; :: thesis: verum

end;

hence ( G c= F & G is finite & [:([#] Y),Q:] c= union G ) by A5, A7; :: thesis: verum

end;

union G is open by A2, A5, TOPS_2:11, TOPS_2:19;
then Q in the topology of X by Th12;
then Q is open by PRE_TOPC:def 2;
then Q in R by A3, A9;
hence k in union R by A8, TARSKI:def 4; :: thesis: verum

end;

hence R is Cover of X by SETFAM_1:def 11; :: thesis: verum