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

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