theorem Th9: :: MSUALG_7:9

for I being non empty set
for M being ManySortedSet of I holds EqRelLatt M is complete