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 A1: ( ( 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 ) ) ; :: thesis: W1 = W2
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;
( W1 = GenMSAlg B & W2 = GenMSAlg B ) by A1;
hence W1 = W2 ; :: thesis: verum