theorem :: PBOOLE:139

for I being set
for M being ManySortedSet of I
for i being object st i in I holds
M . i is Component of M