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