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

for U1 being MSSubAlgebra of U0

for A, B being MSSubset of U0 st B = A (\/) the Sorts of U1 holds

(GenMSAlg A) "\/" U1 = GenMSAlg B

let U0 be non-empty MSAlgebra over S; :: thesis: for U1 being MSSubAlgebra of U0

for A, B being MSSubset of U0 st B = A (\/) the Sorts of U1 holds

(GenMSAlg A) "\/" U1 = GenMSAlg B

let U1 be MSSubAlgebra of U0; :: thesis: for A, B being MSSubset of U0 st B = A (\/) the Sorts of U1 holds

(GenMSAlg A) "\/" U1 = GenMSAlg B

let A, B be MSSubset of U0; :: thesis: ( B = A (\/) the Sorts of U1 implies (GenMSAlg A) "\/" U1 = GenMSAlg B )

reconsider u1 = the Sorts of U1, a = the Sorts of (GenMSAlg A) as MSSubset of U0 by Def9;

A1: the Sorts of (GenMSAlg A) (/\) the Sorts of (GenMSAlg B) c= a by PBOOLE:15;

A2: the Sorts of ((GenMSAlg A) /\ (GenMSAlg B)) = the Sorts of (GenMSAlg A) (/\) the Sorts of (GenMSAlg B) by Def16;

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

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

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

A3: (GenMSAlg A) "\/" U1 = GenMSAlg b by Def18;

then a (\/) u1 is MSSubset of ((GenMSAlg A) "\/" U1) by Def17;

then A4: a (\/) u1 c= the Sorts of ((GenMSAlg A) "\/" U1) by PBOOLE:def 18;

A is MSSubset of (GenMSAlg A) by Def17;

then A5: A c= the Sorts of (GenMSAlg A) by PBOOLE:def 18;

B is MSSubset of (GenMSAlg B) by Def17;

then A6: B c= the Sorts of (GenMSAlg B) by PBOOLE:def 18;

assume A7: B = A (\/) the Sorts of U1 ; :: thesis: (GenMSAlg A) "\/" U1 = GenMSAlg B

then A c= B by PBOOLE:14;

then A c= the Sorts of (GenMSAlg B) by A6, PBOOLE:13;

then A c= the Sorts of (GenMSAlg A) (/\) the Sorts of (GenMSAlg B) by A5, PBOOLE:17;

then A is MSSubset of ((GenMSAlg A) /\ (GenMSAlg B)) by A2, PBOOLE:def 18;

then GenMSAlg A is MSSubAlgebra of (GenMSAlg A) /\ (GenMSAlg B) by Def17;

then a is MSSubset of ((GenMSAlg A) /\ (GenMSAlg B)) by Def9;

then a c= the Sorts of (GenMSAlg A) (/\) the Sorts of (GenMSAlg B) by A2, PBOOLE:def 18;

then a = the Sorts of (GenMSAlg A) (/\) the Sorts of (GenMSAlg B) by A1, PBOOLE:146;

then A8: a c= the Sorts of (GenMSAlg B) by PBOOLE:15;

u1 c= B by A7, PBOOLE:14;

then u1 c= the Sorts of (GenMSAlg B) by A6, PBOOLE:13;

then b c= the Sorts of (GenMSAlg B) by A8, PBOOLE:16;

then b is MSSubset of (GenMSAlg B) by PBOOLE:def 18;

then A9: GenMSAlg b is strict MSSubAlgebra of GenMSAlg B by Def17;

A (\/) u1 c= a (\/) u1 by A5, PBOOLE:20;

then B c= the Sorts of ((GenMSAlg A) "\/" U1) by A7, A4, PBOOLE:13;

then B is MSSubset of ((GenMSAlg A) "\/" U1) by PBOOLE:def 18;

then GenMSAlg B is strict MSSubAlgebra of (GenMSAlg A) "\/" U1 by Def17;

hence (GenMSAlg A) "\/" U1 = GenMSAlg B by A3, A9, Th7; :: thesis: verum

for U1 being MSSubAlgebra of U0

for A, B being MSSubset of U0 st B = A (\/) the Sorts of U1 holds

(GenMSAlg A) "\/" U1 = GenMSAlg B

let U0 be non-empty MSAlgebra over S; :: thesis: for U1 being MSSubAlgebra of U0

for A, B being MSSubset of U0 st B = A (\/) the Sorts of U1 holds

(GenMSAlg A) "\/" U1 = GenMSAlg B

let U1 be MSSubAlgebra of U0; :: thesis: for A, B being MSSubset of U0 st B = A (\/) the Sorts of U1 holds

(GenMSAlg A) "\/" U1 = GenMSAlg B

let A, B be MSSubset of U0; :: thesis: ( B = A (\/) the Sorts of U1 implies (GenMSAlg A) "\/" U1 = GenMSAlg B )

reconsider u1 = the Sorts of U1, a = the Sorts of (GenMSAlg A) as MSSubset of U0 by Def9;

A1: the Sorts of (GenMSAlg A) (/\) the Sorts of (GenMSAlg B) c= a by PBOOLE:15;

A2: the Sorts of ((GenMSAlg A) /\ (GenMSAlg B)) = the Sorts of (GenMSAlg A) (/\) the Sorts of (GenMSAlg B) by Def16;

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

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

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

A3: (GenMSAlg A) "\/" U1 = GenMSAlg b by Def18;

then a (\/) u1 is MSSubset of ((GenMSAlg A) "\/" U1) by Def17;

then A4: a (\/) u1 c= the Sorts of ((GenMSAlg A) "\/" U1) by PBOOLE:def 18;

A is MSSubset of (GenMSAlg A) by Def17;

then A5: A c= the Sorts of (GenMSAlg A) by PBOOLE:def 18;

B is MSSubset of (GenMSAlg B) by Def17;

then A6: B c= the Sorts of (GenMSAlg B) by PBOOLE:def 18;

assume A7: B = A (\/) the Sorts of U1 ; :: thesis: (GenMSAlg A) "\/" U1 = GenMSAlg B

then A c= B by PBOOLE:14;

then A c= the Sorts of (GenMSAlg B) by A6, PBOOLE:13;

then A c= the Sorts of (GenMSAlg A) (/\) the Sorts of (GenMSAlg B) by A5, PBOOLE:17;

then A is MSSubset of ((GenMSAlg A) /\ (GenMSAlg B)) by A2, PBOOLE:def 18;

then GenMSAlg A is MSSubAlgebra of (GenMSAlg A) /\ (GenMSAlg B) by Def17;

then a is MSSubset of ((GenMSAlg A) /\ (GenMSAlg B)) by Def9;

then a c= the Sorts of (GenMSAlg A) (/\) the Sorts of (GenMSAlg B) by A2, PBOOLE:def 18;

then a = the Sorts of (GenMSAlg A) (/\) the Sorts of (GenMSAlg B) by A1, PBOOLE:146;

then A8: a c= the Sorts of (GenMSAlg B) by PBOOLE:15;

u1 c= B by A7, PBOOLE:14;

then u1 c= the Sorts of (GenMSAlg B) by A6, PBOOLE:13;

then b c= the Sorts of (GenMSAlg B) by A8, PBOOLE:16;

then b is MSSubset of (GenMSAlg B) by PBOOLE:def 18;

then A9: GenMSAlg b is strict MSSubAlgebra of GenMSAlg B by Def17;

A (\/) u1 c= a (\/) u1 by A5, PBOOLE:20;

then B c= the Sorts of ((GenMSAlg A) "\/" U1) by A7, A4, PBOOLE:13;

then B is MSSubset of ((GenMSAlg A) "\/" U1) by PBOOLE:def 18;

then GenMSAlg B is strict MSSubAlgebra of (GenMSAlg A) "\/" U1 by Def17;

hence (GenMSAlg A) "\/" U1 = GenMSAlg B by A3, A9, Th7; :: thesis: verum