:: deftheorem Def9 defines MSSubAlgebra MSUALG_2:def 9 :
for S being non empty non void ManySortedSign
for U0, b₃ being MSAlgebra over S holds
( b₃ is MSSubAlgebra of U0 iff ( the Sorts of b₃ is MSSubset of U0 & ( for B being MSSubset of U0 st B = the Sorts of b₃ holds
( B is opers_closed & the Charact of b₃ = Opers (U0,B) ) ) ) );