let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra of S
for A being MSSubset of U0 holds
( GenMSAlg A = U0 | (MSSubSort A) & the Sorts of (GenMSAlg A) = MSSubSort A )
let U0 be MSAlgebra of S; :: thesis: for A being MSSubset of U0 holds
( GenMSAlg A = U0 | (MSSubSort A) & the Sorts of (GenMSAlg A) = MSSubSort A )
let A be MSSubset of U0; :: thesis: ( GenMSAlg A = U0 | (MSSubSort A) & the Sorts of (GenMSAlg A) = MSSubSort A )
set a = MSSubSort A;
reconsider u1 = U0 | (MSSubSort A) as strict MSSubAlgebra of U0 ;
A1: u1 = MSAlgebra(# (MSSubSort A),(Opers U0,(MSSubSort A)) #) by MSUALG_2:21, MSUALG_2:def 16;
A2: A c= MSSubSort A by MSUALG_2:21;
A3: ( A is MSSubset of u1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
u1 is MSSubAlgebra of U1 ) )

proof

thus A is MSSubset of u1 by A2, A1, PBOOLE:def 23; :: thesis: for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
u1 is MSSubAlgebra of U1
let U2 be MSSubAlgebra of U0; :: thesis: ( A is MSSubset of U2 implies u1 is MSSubAlgebra of U2 )
reconsider B = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def 10;
Constants U0 is MSSubset of U2 by MSUALG_2:11;
then A4: Constants U0 c= B by PBOOLE:def 23;
assume A is MSSubset of U2 ; :: thesis: u1 is MSSubAlgebra of U2
then ( B is opers_closed & A c= B ) by MSUALG_2:def 10, PBOOLE:def 23;
then A5: B in SubSort A by A4, MSUALG_2:14;
the Sorts of u1 c= the Sorts of U2

proof

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in the carrier of S or the Sorts of u1 . i c= the Sorts of U2 . i )
assume i in the carrier of S ; :: thesis: the Sorts of u1 . i c= the Sorts of U2 . i
then reconsider s = i as SortSymbol of S ;
( the Sorts of u1 . s = meet (SubSort A,s) & B . s in SubSort A,s ) by A1, A5, MSUALG_2:def 14, MSUALG_2:def 15;
hence the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:4; :: thesis: verum

end;

hence u1 is MSSubAlgebra of U2 by MSUALG_2:9; :: thesis: verum

end;

hence GenMSAlg A = U0 | (MSSubSort A) by MSUALG_2:def 18; :: thesis: the Sorts of (GenMSAlg A) = MSSubSort A
thus the Sorts of (GenMSAlg A) = MSSubSort A by A1, A3, MSUALG_2:def 18; :: thesis: verum