for X, Y being TopSpace
for H being Subset-Family of X
for Y being Subset of X st H is Cover of Y holds
ex F being Subset-Family of X st
( F c= H & F is Cover of Y & ( for C being set st C in F holds
C meets Y ) )