let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra over S
for U1 being MSSubAlgebra of U0
for B being MSSubset of U0 st B = the Sorts of U1 holds
GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #)

let U0 be MSAlgebra over S; :: thesis: for U1 being MSSubAlgebra of U0
for B being MSSubset of U0 st B = the Sorts of U1 holds
GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #)

let U1 be MSSubAlgebra of U0; :: thesis: for B being MSSubset of U0 st B = the Sorts of U1 holds
GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #)

let B be MSSubset of U0; :: thesis: ( B = the Sorts of U1 implies GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #) )
assume A1: B = the Sorts of U1 ; :: thesis: GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #)
set W = GenMSAlg B;
B is MSSubset of () by Def17;
then the Sorts of U1 c= the Sorts of () by ;
then A2: U1 is MSSubAlgebra of GenMSAlg B by Th8;
B is MSSubset of U1 by ;
then GenMSAlg B is MSSubAlgebra of U1 by Def17;
hence GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #) by ; :: thesis: verum