reconsider B1 = the Sorts of U1, B2 = the Sorts of U2 as OrderSortedSet of S1 by OSALG_1:17;
set B = the Sorts of U1 (\/) the Sorts of U2;
the Sorts of U2 is MSSubset of U0 by MSUALG_2:def 9;
then A2: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def 18;
the Sorts of U1 is MSSubset of U0 by MSUALG_2:def 9;
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 OSSubAlgebra of U0; :: thesis: ( ( for A being OSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds
W1 = GenOSAlg A ) & ( for A being OSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds
W2 = GenOSAlg A ) implies W1 = W2 )
assume that
A3: for A being OSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds
W1 = GenOSAlg A and
A4: for A being OSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds
W2 = GenOSAlg A ; :: thesis: W1 = W2
B = B1 (\/) B2 ;
then B is OrderSortedSet of S1 by Th2;
then reconsider B0 = B as OSSubset of U0 by Def2;
W1 = GenOSAlg B0 by A3;
hence W1 = W2 by A4; :: thesis: verum