the Sorts of U1 is OrderSortedSet of S1 by OSALG_1:17;
hence MSAlgebra(# the Sorts of U1, the Charact of U1 #) is order-sorted by OSALG_1:17; :: thesis: verum