for I being set
for i being object
for M being ManySortedSet of I
for SF being MSSubsetFamily of M st i in I holds
SF . i is Subset-Family of (M . i)