let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra of S
for U1 being MSSubAlgebra of U0 holds (GenMSAlg (Constants U0)) /\ U1 = GenMSAlg (Constants U0)
let U0 be non-empty MSAlgebra of 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 Th11;
then GenMSAlg (Constants U0) is strict MSSubAlgebra of U1 by Def18;
then the Sorts of (GenMSAlg (Constants U0)) is MSSubset of U1 by Def10;
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 Def17;
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 Th10; :: thesis: verum