( 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; :: thesis: ( 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 ) ; :: thesis: W1 = W2
the charact of W2 = Opers (U0,C) by A9, A10;
hence W1 = W2 by A8, A9; :: thesis: verum