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 /\ (U1 "\/" U2) = MSAlgebra(# the Sorts of U1, the Charact of U1 #)

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

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

reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by Def9;

A1: the Sorts of (U1 /\ (U1 "\/" U2)) = the Sorts of U1 (/\) the Sorts of (U1 "\/" U2) by Def16;

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

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

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

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

then A is MSSubset of (U1 "\/" U2) by Def17;

then A2: A c= the Sorts of (U1 "\/" U2) by PBOOLE:def 18;

the Sorts of U1 c= A by PBOOLE:14;

then the Sorts of U1 c= the Sorts of (U1 "\/" U2) by A2, PBOOLE:13;

then A3: the Sorts of U1 c= the Sorts of (U1 /\ (U1 "\/" U2)) by A1, PBOOLE:17;

reconsider u112 = the Sorts of (U1 /\ (U1 "\/" U2)) as MSSubset of U0 by Def9;

A4: the Charact of (U1 /\ (U1 "\/" U2)) = Opers (U0,u112) by Def16;

the Sorts of (U1 /\ (U1 "\/" U2)) c= the Sorts of U1 by A1, PBOOLE:15;

then the Sorts of (U1 /\ (U1 "\/" U2)) = the Sorts of U1 by A3, PBOOLE:146;

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

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

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

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

reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by Def9;

A1: the Sorts of (U1 /\ (U1 "\/" U2)) = the Sorts of U1 (/\) the Sorts of (U1 "\/" U2) by Def16;

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

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

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

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

then A is MSSubset of (U1 "\/" U2) by Def17;

then A2: A c= the Sorts of (U1 "\/" U2) by PBOOLE:def 18;

the Sorts of U1 c= A by PBOOLE:14;

then the Sorts of U1 c= the Sorts of (U1 "\/" U2) by A2, PBOOLE:13;

then A3: the Sorts of U1 c= the Sorts of (U1 /\ (U1 "\/" U2)) by A1, PBOOLE:17;

reconsider u112 = the Sorts of (U1 /\ (U1 "\/" U2)) as MSSubset of U0 by Def9;

A4: the Charact of (U1 /\ (U1 "\/" U2)) = Opers (U0,u112) by Def16;

the Sorts of (U1 /\ (U1 "\/" U2)) c= the Sorts of U1 by A1, PBOOLE:15;

then the Sorts of (U1 /\ (U1 "\/" U2)) = the Sorts of U1 by A3, PBOOLE:146;

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