:: deftheorem Def6 defines Algebra ALGSPEC1:def 6 :
for b1 being object holds
( b1 is Algebra iff ex S being non void Signature st b1 is feasible MSAlgebra over S );