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

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