theorem :: MSSUBFAM:45

for I being set
for Z, M being ManySortedSet of I
for SF being V8() MSSubsetFamily of M st ( for Z1 being ManySortedSet of I st Z1 in SF holds
Z c= Z1 ) holds
Z c= meet SF