let S1 be OrderSortedSign; :: thesis: for U0 being non-empty OSAlgebra of S1
for U1 being OSSubAlgebra of U0
for A, B being OSSubset of U0 st B = A (\/) the Sorts of U1 holds
(GenOSAlg A) "\/"_os U1 = GenOSAlg B
let U0 be non-empty OSAlgebra of S1; :: thesis: for U1 being OSSubAlgebra of U0
for A, B being OSSubset of U0 st B = A (\/) the Sorts of U1 holds
(GenOSAlg A) "\/"_os U1 = GenOSAlg B
let U1 be OSSubAlgebra of U0; :: thesis: for A, B being OSSubset of U0 st B = A (\/) the Sorts of U1 holds
(GenOSAlg A) "\/"_os U1 = GenOSAlg B
let A, B be OSSubset of U0; :: thesis: ( B = A (\/) the Sorts of U1 implies (GenOSAlg A) "\/"_os U1 = GenOSAlg B )
assume A1: B = A (\/) the Sorts of U1 ; :: thesis: (GenOSAlg A) "\/"_os U1 = GenOSAlg B
reconsider u1m = the Sorts of U1, am = the Sorts of (GenOSAlg A) as MSSubset of U0 by MSUALG_2:def 9;
A2: ( the Sorts of U1 is OrderSortedSet of S1 & the Sorts of (GenOSAlg A) is OrderSortedSet of S1 ) by OSALG_1:17;
then reconsider u1 = u1m, a = am as OSSubset of U0 by Def2;
( 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: a (\/) u1 is OrderSortedSet of S1 by A2, Th2;
then reconsider b = b as OSSubset of U0 by Def2;
A4: (GenOSAlg A) "\/"_os U1 = GenOSAlg b by Def13;
then a (\/) u1 is OSSubset of (GenOSAlg A) "\/"_os U1 by Def12;
then A5: a (\/) u1 c= the Sorts of ((GenOSAlg A) "\/"_os U1) by PBOOLE:def 18;
A is OSSubset of GenOSAlg A by Def12;
then A6: A c= the Sorts of (GenOSAlg A) by PBOOLE:def 18;
then A (\/) u1 c= a (\/) u1 by PBOOLE:20;
then B c= the Sorts of ((GenOSAlg A) "\/"_os U1) by A1, A5, PBOOLE:13;
then A7: B is MSSubset of ((GenOSAlg A) "\/"_os U1) by PBOOLE:def 18;
A8: A is OrderSortedSet of S1 by Def2;
A9: the Sorts of ((GenOSAlg A) /\ (GenOSAlg B)) = the Sorts of (GenOSAlg A) (/\) the Sorts of (GenOSAlg B) by MSUALG_2:def 16;
B is OSSubset of GenOSAlg B by Def12;
then A10: B c= the Sorts of (GenOSAlg B) by PBOOLE:def 18;
A c= B by A1, PBOOLE:14;
then A c= the Sorts of (GenOSAlg B) by A10, PBOOLE:13;
then A c= the Sorts of (GenOSAlg A) (/\) the Sorts of (GenOSAlg B) by A6, PBOOLE:17;
then A is MSSubset of ((GenOSAlg A) /\ (GenOSAlg B)) by A9, PBOOLE:def 18;
then A is OSSubset of (GenOSAlg A) /\ (GenOSAlg B) by A8, Def2;
then GenOSAlg A is OSSubAlgebra of (GenOSAlg A) /\ (GenOSAlg B) by Def12;
then a is MSSubset of ((GenOSAlg A) /\ (GenOSAlg B)) by MSUALG_2:def 9;
then A11: a c= the Sorts of (GenOSAlg A) (/\) the Sorts of (GenOSAlg B) by A9, PBOOLE:def 18;
the Sorts of (GenOSAlg A) (/\) the Sorts of (GenOSAlg B) c= a by PBOOLE:15;
then a = the Sorts of (GenOSAlg A) (/\) the Sorts of (GenOSAlg B) by A11, PBOOLE:146;
then A12: a c= the Sorts of (GenOSAlg B) by PBOOLE:15;
u1 c= B by A1, PBOOLE:14;
then u1 c= the Sorts of (GenOSAlg B) by A10, PBOOLE:13;
then b c= the Sorts of (GenOSAlg B) by A12, PBOOLE:16;
then b is MSSubset of (GenOSAlg B) by PBOOLE:def 18;
then b is OSSubset of GenOSAlg B by A3, Def2;
then A13: GenOSAlg b is strict OSSubAlgebra of GenOSAlg B by Def12;
B is OrderSortedSet of S1 by Def2;
then B is OSSubset of (GenOSAlg A) "\/"_os U1 by A7, Def2;
then GenOSAlg B is strict OSSubAlgebra of (GenOSAlg A) "\/"_os U1 by Def12;
hence (GenOSAlg A) "\/"_os U1 = GenOSAlg B by A4, A13, MSUALG_2:7; :: thesis: verum