:: deftheorem Def14 defines MSSubSort MSUALG_2:def 14 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A, b₄ being MSSubset of U0 holds
( b₄ = MSSubSort A iff for s being SortSymbol of S holds b₄ . s = meet (SubSort (A,s)) );