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
ex C being Subset-Family of X st
( C c= R & C is finite & C 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
ex C being Subset-Family of X st
( C c= R & C is finite & C 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 ex C being Subset-Family of X st
( C c= R & C is finite & C is Cover of X ) )
assume ( 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: ex C being Subset-Family of X st
( C c= R & C is finite & C is Cover of X )
then ( R is open & R is Cover of X ) by Th18;
then ex G being Subset-Family of X st
( G c= R & G is Cover of X & G is finite ) by COMPTS_1:def 1;
hence ex C being Subset-Family of X st
( C c= R & C is finite & C is Cover of X ) ; :: thesis: verum