:: deftheorem Def13 defines SubSort MSUALG_2:def 13 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0
for s being SortSymbol of S
for b₅ being set holds
( b₅ = SubSort (A,s) iff for x being object holds
( x in b₅ iff ex B being MSSubset of U0 st
( B in SubSort A & x = B . s ) ) );