theorem Th31: :: CLOSURE1:31

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 ex 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 ) )