for S being OrderSortedSign
for U0 being OSAlgebra of S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted