let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S

for U1, U2 being MSSubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

let U0 be non-empty MSAlgebra over S; :: thesis: for U1, U2 being MSSubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

let U1, U2 be MSSubAlgebra of U0; :: thesis: (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

reconsider u12 = the Sorts of (U1 /\ U2), u2 = the Sorts of U2 as MSSubset of U0 by Def9;

( u12 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def 18;

then u12 (\/) u2 c= the Sorts of U0 by PBOOLE:16;

then reconsider A = u12 (\/) u2 as MSSubset of U0 by PBOOLE:def 18;

u12 = the Sorts of U1 (/\) the Sorts of U2 by Def16;

then u12 c= u2 by PBOOLE:15;

then A1: A = u2 by PBOOLE:22;

(U1 /\ U2) "\/" U2 = GenMSAlg A by Def18;

hence (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #) by A1, Th22; :: thesis: verum

for U1, U2 being MSSubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

let U0 be non-empty MSAlgebra over S; :: thesis: for U1, U2 being MSSubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

let U1, U2 be MSSubAlgebra of U0; :: thesis: (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #)

reconsider u12 = the Sorts of (U1 /\ U2), u2 = the Sorts of U2 as MSSubset of U0 by Def9;

( u12 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def 18;

then u12 (\/) u2 c= the Sorts of U0 by PBOOLE:16;

then reconsider A = u12 (\/) u2 as MSSubset of U0 by PBOOLE:def 18;

u12 = the Sorts of U1 (/\) the Sorts of U2 by Def16;

then u12 c= u2 by PBOOLE:15;

then A1: A = u2 by PBOOLE:22;

(U1 /\ U2) "\/" U2 = GenMSAlg A by Def18;

hence (U1 /\ U2) "\/" U2 = MSAlgebra(# the Sorts of U2, the Charact of U2 #) by A1, Th22; :: thesis: verum