set B = the Sorts of U1 \/ the Sorts of U2;
( the Sorts of U1 is MSSubset of U0 & the Sorts of U2 is MSSubset of U0 ) by MSUALG_2:def 10;
then ( the Sorts of U1 c= the Sorts of U0 & the Sorts of U2 c= the Sorts of U0 ) by PBOOLE:def 23;
then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by PBOOLE:18;
then reconsider B = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def 23;
reconsider B1 = the Sorts of U1, B2 = the Sorts of U2 as OrderSortedSet of by OSALG_1:17;
B = B1 \/ B2 ;
then B is OrderSortedSet of by Th2;
then reconsider B0 = B as OSSubset of U0 by Def2;
take GenOSAlg B0 ; :: thesis: for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
GenOSAlg B0 = GenOSAlg A
thus for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
GenOSAlg B0 = GenOSAlg A ; :: thesis: verum