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

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