( the carrier of U1 is Subset of U0 & the carrier of U1 /\ the carrier of U2 c= the carrier of U1 )
by Def7, XBOOLE_1:17;
then reconsider C = the carrier of U1 /\ the carrier of U2 as non empty Subset of U0 by A1, XBOOLE_1:1;
let W1, W2 be strict SubAlgebra of U0; ( the carrier of W1 = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of W1 holds
( the charact of W1 = Opers (U0,B) & B is opers_closed ) ) & the carrier of W2 = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of W2 holds
( the charact of W2 = Opers (U0,B) & B is opers_closed ) ) implies W1 = W2 )
assume that
A8:
( the carrier of W1 = the carrier of U1 /\ the carrier of U2 & ( for B1 being non empty Subset of U0 st B1 = the carrier of W1 holds
( the charact of W1 = Opers (U0,B1) & B1 is opers_closed ) ) )
and
A9:
the carrier of W2 = the carrier of U1 /\ the carrier of U2
and
A10:
for B2 being non empty Subset of U0 st B2 = the carrier of W2 holds
( the charact of W2 = Opers (U0,B2) & B2 is opers_closed )
; W1 = W2
the charact of W2 = Opers (U0,C)
by A9, A10;
hence
W1 = W2
by A8, A9; verum