theorem :: CLOSURE1:2

for I being set
for M being ManySortedSet of I st ex A being ManySortedSet of I st A in M holds
M is non-empty ;