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 Def7;
then reconsider B = B as non empty Subset of U0 by XBOOLE_1:8;
take GenUnivAlg B ; :: thesis: for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds
GenUnivAlg B = GenUnivAlg A
thus for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds
GenUnivAlg B = GenUnivAlg A ; :: thesis: verum