( 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

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