:: deftheorem Def19 defines MSSub MSUALG_2:def 19 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for b₃ being set holds
( b₃ = MSSub U0 iff for x being object holds
( x in b₃ iff x is strict MSSubAlgebra of U0 ) );