set E = the non void Extension of S;
set A = the feasible MSAlgebra of the non void Extension of S;
the feasible MSAlgebra of 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 of E ; :: thesis: verum