reconsider B = the carrier of U1 \/ the carrier of U2 as non empty set ;

let W1, W2 be strict SubAlgebra of U0; :: thesis: ( ( for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds

W1 = GenUnivAlg A ) & ( for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds

W2 = GenUnivAlg A ) implies W1 = W2 )

assume that

A1: for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds

W1 = GenUnivAlg A and

A2: for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds

W2 = GenUnivAlg A ; :: thesis: W1 = W2

( the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0 ) by Def7;

then reconsider B = B as non empty Subset of U0 by XBOOLE_1:8;

W1 = GenUnivAlg B by A1;

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

let W1, W2 be strict SubAlgebra of U0; :: thesis: ( ( for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds

W1 = GenUnivAlg A ) & ( for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds

W2 = GenUnivAlg A ) implies W1 = W2 )

assume that

A1: for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds

W1 = GenUnivAlg A and

A2: for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds

W2 = GenUnivAlg A ; :: thesis: W1 = W2

( the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0 ) by Def7;

then reconsider B = B as non empty Subset of U0 by XBOOLE_1:8;

W1 = GenUnivAlg B by A1;

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