theorem Th23: :: CLOSURE2:23

for I being set
for M being ManySortedSet of I
for SF being SubsetFamily of M
for E, T being Element of Bool M st SF = {E,T} holds
meet |:SF:| = E (/\) T