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 A1: ( 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 ) } ) ; :: thesis: ( R is open & R is Cover of X )
then A2: union F = [#] [:Y,X:] by SETFAM_1:60;

now

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

end;

hence R is open by TOPS_2:def 1; :: thesis: R is Cover of X
[#] X c= union R

proof

let k be set ; :: 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 k' = k as Point of X ;
reconsider Z = [:([#] Y),{k'}:] as Subset of [:Y,X:] ;
A4: F is Cover of Z by A2, SETFAM_1:def 12;
Z is compact by Th18;
then consider G being Subset-Family of [:Y,X:] such that
A5: ( G c= F & G is Cover of Z & G is finite ) by A1, A4, COMPTS_1:def 7;
A6: Z c= union G by A5, SETFAM_1:def 12;
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 set ; :: 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 consider x1 being Point of X such that
A7: ( k = x1 & [:([#] Y),{x1}:] c= union G ) ;
thus k in the carrier of X by A7; :: thesis: verum

end;

then reconsider Q = { x where x is Point of X : [:([#] Y),{x}:] c= union G } as Subset of X ;
union G is open by A1, A5, TOPS_2:18, TOPS_2:26;
then Q in the topology of X by Th14;
then A8: Q is open by PRE_TOPC:def 5;
A9: k' in Q by A6;
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 set ; :: 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 set such that
A10: ( x1 in [#] Y & x2 in Q & z = [x1,x2] ) by ZFMISC_1:def 2;
consider x2' being Point of X such that
A11: ( x2' = x2 & [:([#] Y),{x2'}:] c= union G ) by A10;
x2 in {x2'} by A11, TARSKI:def 1;
then z in [:([#] Y),{x2'}:] by A10, ZFMISC_1:106;
hence z in union G by A11; :: thesis: verum

end;

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

end;

then Q in R by A1, A8;
hence k in union R by A9, TARSKI:def 4; :: thesis: verum

end;

then union R = [#] X by XBOOLE_0:def 10;
hence R is Cover of X by SETFAM_1:def 12; :: thesis: verum