A2: the carrier of U1 /\ the carrier of U2 c= the carrier of U1 by XBOOLE_1:17;
the carrier of U1 is Subset of U0 by Def7;
then reconsider C = the carrier of U1 /\ the carrier of U2 as non empty Subset of U0 by ;
set S = UAStr(# C,(Opers (U0,C)) #);
A3: the carrier of U1 /\ the carrier of U2 c= the carrier of U2 by XBOOLE_1:17;
A4: now :: thesis: for o being operation of U0 holds C is_closed_on o
let o be operation of U0; :: thesis:
now :: thesis: for s being FinSequence of C st len s = arity o holds
o . s in C
set B1 = the carrier of U1;
set B2 = the carrier of U2;
let s be FinSequence of C; :: thesis: ( len s = arity o implies o . s in C )
reconsider s2 = s as FinSequence of the carrier of U2 by ;
reconsider s1 = s as FinSequence of the carrier of U1 by ;
assume A5: len s = arity o ; :: thesis: o . s in C
reconsider B1 = the carrier of U1 as non empty Subset of U0 by Def7;
reconsider B2 = the carrier of U2 as non empty Subset of U0 by Def7;
B2 is opers_closed by Def7;
then B2 is_closed_on o ;
then A6: o . s2 in B2 by A5;
B1 is opers_closed by Def7;
then B1 is_closed_on o ;
then o . s1 in B1 by A5;
hence o . s in C by ; :: thesis: verum
end;
hence C is_closed_on o ; :: thesis: verum
end;
then 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 ) ;
reconsider S = UAStr(# C,(Opers (U0,C)) #) as Universal_Algebra by Th14;
reconsider S = S as strict SubAlgebra of U0 by ;
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; :: thesis: verum