set A = the Sorts of U0;
reconsider A = the Sorts of U0 as MSSubset of U0 by PBOOLE:def 18;
take A ; :: thesis: the Sorts of (GenMSAlg A) = the Sorts of U0
set G = GenMSAlg A;
the Sorts of (GenMSAlg A) is MSSubset of U0 by MSUALG_2:def 9;
then A1: the Sorts of (GenMSAlg A) c= A by PBOOLE:def 18;
A is MSSubset of (GenMSAlg A) by MSUALG_2:def 17;
then A c= the Sorts of (GenMSAlg A) by PBOOLE:def 18;
hence the Sorts of (GenMSAlg A) = the Sorts of U0 by A1, PBOOLE:146; :: thesis: verum