:: deftheorem Def17 defines GenMSAlg MSUALG_2:def 17 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubset of U0
for b₄ being strict MSSubAlgebra of U0 holds
( b₄ = GenMSAlg A iff ( A is MSSubset of b₄ & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
b₄ is MSSubAlgebra of U1 ) ) );