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