for X, Y being non empty TopSpace
for F being Subset-Family of X
for H being Subset-Family of [:X,Y:] st F is finite & F c= (Pr1 (X,Y)) .: H holds
ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 (X,Y)) .: G )