let X, Y be non empty compact TopSpace; 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; 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:]; ( 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 ) } )
; 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 )
; verum