let S be OrderSortedSign; :: thesis: for U0 being OSAlgebra of S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted
let U0 be OSAlgebra of S; :: thesis: MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted
the Sorts of U0 is OrderSortedSet of S by OSALG_1:17;
hence MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted by OSALG_1:17; :: thesis: verum