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