theorem Th4: :: OSALG_2:4

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