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
A1: S is Extension of S by Th47;
A is Algebra by Def6;
hence A is Algebra of S by A1, Def7; :: thesis: verum