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 A1: ( ( 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 ) ) ; :: thesis: W1 = W2
reconsider B = the carrier of U1 \/ the carrier of U2 as non empty set ;
( the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0 ) by Def8;
then reconsider B = B as non empty Subset of U0 by XBOOLE_1:8;
( W1 = GenUnivAlg B & W2 = GenUnivAlg B ) by A1;
hence W1 = W2 ; :: thesis: verum