let S be non void Signature; :: thesis: for A being feasible MSAlgebra of S holds A is Algebra of S
let A be feasible MSAlgebra of S; :: thesis: A is Algebra of S
( A is Algebra & S is Extension of S ) by Def6, Th47;
hence A is Algebra of S by Def7; :: thesis: verum