let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra of S
for U1 being strict MSSubAlgebra of U0
for B being MSSubset of U0 st B = the Sorts of U1 holds
GenMSAlg B = U1
let U0 be MSAlgebra of S; :: thesis: for U1 being strict MSSubAlgebra of U0
for B being MSSubset of U0 st B = the Sorts of U1 holds
GenMSAlg B = U1
let U1 be strict MSSubAlgebra of U0; :: thesis: for B being MSSubset of U0 st B = the Sorts of U1 holds
GenMSAlg B = U1
let B be MSSubset of U0; :: thesis: ( B = the Sorts of U1 implies GenMSAlg B = U1 )
assume A1: B = the Sorts of U1 ; :: thesis: GenMSAlg B = U1
set W = GenMSAlg B;
B is MSSubset of (GenMSAlg B) by Def18;
then the Sorts of U1 c= the Sorts of (GenMSAlg B) by A1, PBOOLE:def 18;
then A2: U1 is strict MSSubAlgebra of GenMSAlg B by Th9;
B is MSSubset of U1 by A1, PBOOLE:def 18;
then GenMSAlg B is strict MSSubAlgebra of U1 by Def18;
hence GenMSAlg B = U1 by A2, Th8; :: thesis: verum