set B = the Sorts of U1 (\/) the Sorts of U2;

the Sorts of U2 is MSSubset of U0 by Def9;

then A2: 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 A2, PBOOLE:16;

then reconsider B = the Sorts of U1 (\/) the Sorts of U2 as MSSubset of U0 by PBOOLE:def 18;

let W1, W2 be strict MSSubAlgebra of U0; :: thesis: ( ( for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds

W1 = GenMSAlg A ) & ( for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds

W2 = GenMSAlg A ) implies W1 = W2 )

assume that

A3: for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds

W1 = GenMSAlg A and

A4: for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds

W2 = GenMSAlg A ; :: thesis: W1 = W2

W1 = GenMSAlg B by A3;

hence W1 = W2 by A4; :: thesis: verum

the Sorts of U2 is MSSubset of U0 by Def9;

then A2: 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 A2, PBOOLE:16;

then reconsider B = the Sorts of U1 (\/) the Sorts of U2 as MSSubset of U0 by PBOOLE:def 18;

let W1, W2 be strict MSSubAlgebra of U0; :: thesis: ( ( for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds

W1 = GenMSAlg A ) & ( for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds

W2 = GenMSAlg A ) implies W1 = W2 )

assume that

A3: for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds

W1 = GenMSAlg A and

A4: for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds

W2 = GenMSAlg A ; :: thesis: W1 = W2

W1 = GenMSAlg B by A3;

hence W1 = W2 by A4; :: thesis: verum