let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra over S

for B being MSSubset of U0 st B = the Sorts of U0 holds

GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #)

let U0 be MSAlgebra over S; :: thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds

GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #)

let B be MSSubset of U0; :: thesis: ( B = the Sorts of U0 implies GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #) )

set W = GenMSAlg B;

reconsider B1 = the Sorts of (GenMSAlg B) as MSSubset of U0 by Def9;

A1: the Charact of (GenMSAlg B) = Opers (U0,B1) by Def9;

assume B = the Sorts of U0 ; :: thesis: GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #)

then the Sorts of U0 is MSSubset of (GenMSAlg B) by Def17;

then A2: the Sorts of U0 c= the Sorts of (GenMSAlg B) by PBOOLE:def 18;

the Sorts of (GenMSAlg B) is MSSubset of U0 by Def9;

then the Sorts of (GenMSAlg B) c= the Sorts of U0 by PBOOLE:def 18;

then the Sorts of U0 = the Sorts of (GenMSAlg B) by A2, PBOOLE:146;

hence GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #) by A1, Th4; :: thesis: verum

for B being MSSubset of U0 st B = the Sorts of U0 holds

GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #)

let U0 be MSAlgebra over S; :: thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds

GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #)

let B be MSSubset of U0; :: thesis: ( B = the Sorts of U0 implies GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #) )

set W = GenMSAlg B;

reconsider B1 = the Sorts of (GenMSAlg B) as MSSubset of U0 by Def9;

A1: the Charact of (GenMSAlg B) = Opers (U0,B1) by Def9;

assume B = the Sorts of U0 ; :: thesis: GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #)

then the Sorts of U0 is MSSubset of (GenMSAlg B) by Def17;

then A2: the Sorts of U0 c= the Sorts of (GenMSAlg B) by PBOOLE:def 18;

the Sorts of (GenMSAlg B) is MSSubset of U0 by Def9;

then the Sorts of (GenMSAlg B) c= the Sorts of U0 by PBOOLE:def 18;

then the Sorts of U0 = the Sorts of (GenMSAlg B) by A2, PBOOLE:146;

hence GenMSAlg B = MSAlgebra(# the Sorts of U0, the Charact of U0 #) by A1, Th4; :: thesis: verum