:: deftheorem Def16 defines /\ MSUALG_2:def 16 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0
for b₅ being strict MSSubAlgebra of U0 holds
( b₅ = U1 /\ U2 iff ( the Sorts of b₅ = the Sorts of U1 (/\) the Sorts of U2 & ( for B being MSSubset of U0 st B = the Sorts of b₅ holds
( B is opers_closed & the Charact of b₅ = Opers (U0,B) ) ) ) );