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

( 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