:: deftheorem Def11 defines SubSort MSUALG_2:def 11 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for b₃ being set holds
( b₃ = SubSort U0 iff for x being object holds
( x in b₃ iff ( x in Funcs ( the carrier of S,(bool (Union the Sorts of U0))) & x is MSSubset of U0 & ( for B being MSSubset of U0 st B = x holds
B is opers_closed ) ) ) );