let S be non void Signature; :: thesis: for A being feasible MSAlgebra over S holds A is Algebra of S
let A be feasible MSAlgebra over S; :: thesis: A is Algebra of S
A1: S is Extension of S by Th45;
A is Algebra by Def6;
hence A is Algebra of S by A1, Def7; :: thesis: verum