for X, Y, x being set
for S being Subset-Family of Y
for f being Function of X,Y st x in meet ((" f) .: S) holds
f . x in meet S