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

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