for X, Y being set
for S being cap-closed Subset-Family of X
for f being Function of X,Y st f is one-to-one holds
f .: S is cap-closed Subset-Family of Y