:: deftheorem Def7 defines Algebra ALGSPEC1:def 7 :
for S being Signature
for b₂ being Algebra holds
( b₂ is Algebra of S iff ex E being non void Extension of S st b₂ is feasible MSAlgebra over E );