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