theorem :: BORSUK_3:17

for X, Y being non empty compact TopSpace
for R being Subset-Family of X st R = { Q where Q is open Subset of X : [:([#] Y),Q:] c= union (Base-Appr ([#] [:Y,X:])) } holds
( R is open & R is Cover of [#] X )