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
() "\/" 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
() "\/" 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
() "\/" U1 = GenMSAlg B

let A, B be MSSubset of U0; :: thesis: ( B = A (\/) the Sorts of U1 implies () "\/" U1 = GenMSAlg B )
reconsider u1 = the Sorts of U1, a = the Sorts of () as MSSubset of U0 by Def9;
A1: the Sorts of () (/\) the Sorts of () c= a by PBOOLE:15;
A2: the Sorts of (() /\ ()) = the Sorts of () (/\) the Sorts of () 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 (() "\/" U1) by Def17;
then A4: a (\/) u1 c= the Sorts of (() "\/" U1) by PBOOLE:def 18;
A is MSSubset of () by Def17;
then A5: A c= the Sorts of () by PBOOLE:def 18;
B is MSSubset of () by Def17;
then A6: B c= the Sorts of () by PBOOLE:def 18;
assume A7: B = A (\/) the Sorts of U1 ; :: thesis: () "\/" U1 = GenMSAlg B
then A c= B by PBOOLE:14;
then A c= the Sorts of () by ;
then A c= the Sorts of () (/\) the Sorts of () by ;
then A is MSSubset of (() /\ ()) by ;
then GenMSAlg A is MSSubAlgebra of () /\ () by Def17;
then a is MSSubset of (() /\ ()) by Def9;
then a c= the Sorts of () (/\) the Sorts of () by ;
then a = the Sorts of () (/\) the Sorts of () by ;
then A8: a c= the Sorts of () by PBOOLE:15;
u1 c= B by ;
then u1 c= the Sorts of () by ;
then b c= the Sorts of () by ;
then b is MSSubset of () by PBOOLE:def 18;
then A9: GenMSAlg b is strict MSSubAlgebra of GenMSAlg B by Def17;
A (\/) u1 c= a (\/) u1 by ;
then B c= the Sorts of (() "\/" U1) by ;
then B is MSSubset of (() "\/" U1) by PBOOLE:def 18;
then GenMSAlg B is strict MSSubAlgebra of () "\/" U1 by Def17;
hence (GenMSAlg A) "\/" U1 = GenMSAlg B by A3, A9, Th7; :: thesis: verum