theorem Th7: :: OSALG_2:7

for S1 being OrderSortedSign
for M being ManySortedSet of the carrier of S1 holds M c= OSCl M