for f being Function st dom f is subset-closed & dom f is d.union-closed & f is d.union-distributive holds
for a, y being set st a in dom f & y in f . a holds
ex b being set st
( b is finite & b c= a & y in f . b )