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