A2: ( the carrier of U1 is Subset of U0 & the carrier of U2 is Subset of U0 ) by Def8;
A3: ( the carrier of U1 /\ the carrier of U2 c= the carrier of U1 & the carrier of U1 /\ the carrier of U2 c= the carrier of U2 ) by XBOOLE_1:17;
then reconsider C = the carrier of U1 /\ the carrier of U2 as non empty Subset of U0 by A1, A2, XBOOLE_0:def 7, XBOOLE_1:1;

A4: now

let o be operation of U0; :: thesis: C is_closed_on o

now

let s be FinSequence of C; :: thesis: ( len s = arity o implies o . s in C )
assume A5: len s = arity o ; :: thesis: o . s in C
set B1 = the carrier of U1;
set B2 = the carrier of U2;
reconsider s1 = s as FinSequence of the carrier of U1 by A3, FINSEQ_2:27;
reconsider B1 = the carrier of U1 as non empty Subset of U0 by Def8;
B1 is opers_closed by Def8;
then B1 is_closed_on o by Def5;
then A6: o . s1 in B1 by A5, Def4;
reconsider s2 = s as FinSequence of the carrier of U2 by A3, FINSEQ_2:27;
reconsider B2 = the carrier of U2 as non empty Subset of U0 by Def8;
B2 is opers_closed by Def8;
then B2 is_closed_on o by Def5;
then o . s2 in B2 by A5, Def4;
hence o . s in C by A6, XBOOLE_0:def 4; :: thesis: verum

end;

hence C is_closed_on o by Def4; :: thesis: verum

end;

set S = UAStr(# C,(Opers U0,C) #);
A7: for B being non empty Subset of U0 st B = the carrier of UAStr(# C,(Opers U0,C) #) holds
( the charact of UAStr(# C,(Opers U0,C) #) = Opers U0,B & B is opers_closed ) by A4, Def5;
reconsider S = UAStr(# C,(Opers U0,C) #) as Universal_Algebra by Th17;
reconsider S = S as strict SubAlgebra of U0 by A7, Def8;
take S ; :: thesis: ( the carrier of S = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of S holds
( the charact of S = Opers U0,B & B is opers_closed ) ) )
thus ( the carrier of S = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of S holds
( the charact of S = Opers U0,B & B is opers_closed ) ) ) by A4, Def5; :: thesis: verum