for X, Y being 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 )