let S be non empty non void ManySortedSign ; :: thesis: for U1 being MSAlgebra over S
for A, B being MSSubset of U1 st A is ManySortedSubset of B holds
GenMSAlg A is MSSubAlgebra of GenMSAlg B
let U1 be MSAlgebra over S; :: thesis: for A, B being MSSubset of U1 st A is ManySortedSubset of B holds
GenMSAlg A is MSSubAlgebra of GenMSAlg B
let A, B be MSSubset of U1; :: thesis: ( A is ManySortedSubset of B implies GenMSAlg A is MSSubAlgebra of GenMSAlg B )
B is MSSubset of (GenMSAlg B) by MSUALG_2:def 17;
then A1: B c= the Sorts of (GenMSAlg B) by PBOOLE:def 18;
assume A is ManySortedSubset of B ; :: thesis: GenMSAlg A is MSSubAlgebra of GenMSAlg B
then A c= B by PBOOLE:def 18;
then A c= the Sorts of (GenMSAlg B) by A1, PBOOLE:13;
then A is MSSubset of (GenMSAlg B) by PBOOLE:def 18;
hence GenMSAlg A is MSSubAlgebra of GenMSAlg B by MSUALG_2:def 17; :: thesis: verum