let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S
for U1 being MSSubAlgebra of U0 holds (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0)
let U0 be non-empty MSAlgebra over S; :: thesis: for U1 being MSSubAlgebra of U0 holds (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0)
let U1 be MSSubAlgebra of U0; :: thesis: (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0)
set C = Constants U0;
set G = GenMSAlg (Constants U0);
Constants U0 is MSSubset of U1 by Th10;
then GenMSAlg (Constants U0) is strict MSSubAlgebra of U1 by Def17;
then the Sorts of (GenMSAlg (Constants U0)) is MSSubset of U1 by Def9;
then A1: the Sorts of (GenMSAlg (Constants U0)) c= the Sorts of U1 by PBOOLE:def 18;
the Sorts of ((GenMSAlg (Constants U0)) /\ U1) = the Sorts of (GenMSAlg (Constants U0)) (/\) the Sorts of U1 by Def16;
then the Sorts of ((GenMSAlg (Constants U0)) /\ U1) = the Sorts of (GenMSAlg (Constants U0)) by A1, PBOOLE:23;
hence (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0) by Th9; :: thesis: verum