theorem Th1: :: MSUALG_7:1

for I being non empty set
for M being ManySortedSet of I holds id M is Equivalence_Relation of M