let S be non empty non void ManySortedSign ; :: thesis: for U0 being strict MSAlgebra of S
for B being MSSubset of U0 st B = the Sorts of U0 holds
GenMSAlg B = U0
let U0 be strict MSAlgebra of S; :: thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds
GenMSAlg B = U0
let B be MSSubset of U0; :: thesis: ( B = the Sorts of U0 implies GenMSAlg B = U0 )
set W = GenMSAlg B;
reconsider B1 = the Sorts of (GenMSAlg B) as MSSubset of U0 by Def10;
A1: the Charact of (GenMSAlg B) = Opers (U0,B1) by Def10;
assume B = the Sorts of U0 ; :: thesis: GenMSAlg B = U0
then the Sorts of U0 is MSSubset of (GenMSAlg B) by Def18;
then A2: the Sorts of U0 c= the Sorts of (GenMSAlg B) by PBOOLE:def 23;
the Sorts of (GenMSAlg B) is MSSubset of U0 by Def10;
then the Sorts of (GenMSAlg B) c= the Sorts of U0 by PBOOLE:def 23;
then the Sorts of U0 = the Sorts of (GenMSAlg B) by A2, PBOOLE:def 13;
hence GenMSAlg B = U0 by A1, Th5; :: thesis: verum