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 (GenMSAlg B) by Def17;
then the Sorts of U1 c= the Sorts of (GenMSAlg B) by A1, PBOOLE:def 18;
then A2: U1 is MSSubAlgebra of GenMSAlg B by Th8;
B is MSSubset of U1 by A1, PBOOLE:def 18;
then GenMSAlg B is MSSubAlgebra of U1 by Def17;
hence GenMSAlg B = MSAlgebra(# the Sorts of U1, the Charact of U1 #) by A2, Th7; :: thesis: verum