theorem Th14: :: CLOSURE2:14

for I being set
for M being ManySortedSet of I
for SF being SubsetFamily of M st not SF is empty holds
for i being set st i in I holds
|:SF:| . i = { (x . i) where x is Element of Bool M : x in SF }