let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra of 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 of 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 Def10;
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 Def17;
( 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 Def19;
then a \/ u1 is MSSubset of ((GenMSAlg A) "\/" U1) by Def18;
then A4: a \/ u1 c= the Sorts of ((GenMSAlg A) "\/" U1) by PBOOLE:def 18;
A is MSSubset of (GenMSAlg A) by Def18;
then A5: A c= the Sorts of (GenMSAlg A) by PBOOLE:def 18;
B is MSSubset of (GenMSAlg B) by Def18;
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 Def18;
then a is MSSubset of ((GenMSAlg A) /\ (GenMSAlg B)) by Def10;
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:def 10;
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 Def18;
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 Def18;
hence (GenMSAlg A) "\/" U1 = GenMSAlg B by A3, A9, Th8; :: thesis: verum