set B = the Sorts of U1 (\/) the Sorts of U2;
the Sorts of U2 is MSSubset of U0 by Def9;
then A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def 18;
the Sorts of U1 is MSSubset of U0 by Def9;
then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def 18;
then the Sorts of U1 (\/) the Sorts of U2 c= the Sorts of U0 by A1, PBOOLE:16;
then reconsider B = the Sorts of U1 (\/) the Sorts of U2 as MSSubset of U0 by PBOOLE:def 18;
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