theorem Th32: :: CLOSURE1:32

for I being set
for M being ManySortedSet of I
for D being properly-upper-bound MSSubsetFamily of M
for X being Element of bool M
for SF being non-empty MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
for i being set
for Di being non empty set st i in I & Di = D . i holds
SF . i = { z where z is Element of Di : X . i c= z }