:: deftheorem Def9 defines /\ UNIALG_2:def 9 :
for U0 being Universal_Algebra
for U1, U2 being SubAlgebra of U0 st the carrier of U1 meets the carrier of U2 holds
for b₄ being strict SubAlgebra of U0 holds
( b₄ = U1 /\ U2 iff ( the carrier of b₄ = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of b₄ holds
( the charact of b₄ = Opers (U0,B) & B is opers_closed ) ) ) );