let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S
for U1 being MSSubAlgebra of U0
for B being MSSubset of U0 st B = the Sorts of U0 holds
(GenMSAlg B) "\/" U1 = GenMSAlg B
let U0 be non-empty MSAlgebra over S; :: thesis: for U1 being MSSubAlgebra of U0
for B being MSSubset of U0 st B = the Sorts of U0 holds
(GenMSAlg B) "\/" U1 = GenMSAlg B
let U1 be MSSubAlgebra of U0; :: thesis: for B being MSSubset of U0 st B = the Sorts of U0 holds
(GenMSAlg B) "\/" U1 = GenMSAlg B
let B be MSSubset of U0; :: thesis: ( B = the Sorts of U0 implies (GenMSAlg B) "\/" U1 = GenMSAlg B )
assume A1: B = the Sorts of U0 ; :: thesis: (GenMSAlg B) "\/" U1 = GenMSAlg B
the Sorts of U1 is MSSubset of U0 by Def9;
then the Sorts of U1 c= B by A1, PBOOLE:def 18;
then B (\/) the Sorts of U1 = B by PBOOLE:22;
hence (GenMSAlg B) "\/" U1 = GenMSAlg B by Th24; :: thesis: verum