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 Def10;
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;
take GenMSAlg B ; :: thesis: for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
GenMSAlg B = GenMSAlg A
thus for A being MSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
GenMSAlg B = GenMSAlg A ; :: thesis: verum