theorem :: CLOSURE1:11

for I being set
for M being ManySortedSet of I
for X being Element of bool M
for i, x being set st i in I & x in ((id (bool M)) .. X) . i holds
ex Y being finite-yielding Element of bool M st
( Y c= X & x in ((id (bool M)) .. Y) . i )