theorem KeyLemma: :: ROUGHS_3:2

for f being Function st dom f is subset-closed & f is union-distributive & dom f is d.union-closed holds
for a, y being set st a in dom f & y in f . a holds
ex x being set st
( x in a & y in f . {x} )