set E = the non void Extension of S;
set A = the feasible MSAlgebra over the non void Extension of S;
the feasible MSAlgebra over the non void Extension of S is Algebra by Def6;
hence ex b₁ being Algebra ex E being non void Extension of S st b₁ is feasible MSAlgebra over E ; :: thesis: verum