let S be non empty non void ManySortedSign ; :: thesis: for U1 being MSAlgebra over S
for U2 being MSSubAlgebra of U1
for B1 being MSSubset of U1
for B2 being MSSubset of U2 st B1 = B2 holds
GenMSAlg B1 = GenMSAlg B2
let U1 be MSAlgebra over S; :: thesis: for U2 being MSSubAlgebra of U1
for B1 being MSSubset of U1
for B2 being MSSubset of U2 st B1 = B2 holds
GenMSAlg B1 = GenMSAlg B2
let U2 be MSSubAlgebra of U1; :: thesis: for B1 being MSSubset of U1
for B2 being MSSubset of U2 st B1 = B2 holds
GenMSAlg B1 = GenMSAlg B2
let B1 be MSSubset of U1; :: thesis: for B2 being MSSubset of U2 st B1 = B2 holds
GenMSAlg B1 = GenMSAlg B2
let B2 be MSSubset of U2; :: thesis: ( B1 = B2 implies GenMSAlg B1 = GenMSAlg B2 )
assume A1: B1 = B2 ; :: thesis: GenMSAlg B1 = GenMSAlg B2
reconsider H = GenMSAlg B1 as MSSubAlgebra of U2 by A1, MSUALG_2:def 17;
reconsider G = GenMSAlg B2 as MSSubAlgebra of U1 by MSUALG_2:6;
B1 is MSSubset of G by A1, MSUALG_2:def 17;
then A2: GenMSAlg B1 is MSSubAlgebra of G by MSUALG_2:def 17;
B1 is MSSubset of H by MSUALG_2:def 17;
then GenMSAlg B2 is MSSubAlgebra of GenMSAlg B1 by A1, MSUALG_2:def 17;
hence GenMSAlg B1 = GenMSAlg B2 by A2, MSUALG_2:7; :: thesis: verum