:: deftheorem Def2 defines SuperAlgebraSet EQUATION:def 2 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for B being MSSubAlgebra of A
for b₄ being set holds
( b₄ = SuperAlgebraSet B iff for x being object holds
( x in b₄ iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) ) );