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

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