reconsider M1 = the Sorts of OU1, M2 = the Sorts of OU2 as OrderSortedSet of by OSALG_1:17;
M1 /\ M2 is OrderSortedSet of by Th1;
then the Sorts of (OU1 /\ OU2) is OrderSortedSet of by MSUALG_2:def 17;
hence OU1 /\ OU2 is order-sorted by OSALG_1:17; :: thesis: verum