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 10;
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 23;
then a \/ u1 c= the Sorts of U0 by PBOOLE:18;
then reconsider b = a \/ u1 as MSSubset of U0 by PBOOLE:def 23;
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 Def14;
then a \/ u1 is OSSubset of (GenOSAlg A) "\/"_os U1 by Def13;
then A5: a \/ u1 c= the Sorts of ((GenOSAlg A) "\/"_os U1) by PBOOLE:def 23;
A is OSSubset of GenOSAlg A by Def13;
then A6: A c= the Sorts of (GenOSAlg A) by PBOOLE:def 23;
then A \/ u1 c= a \/ u1 by PBOOLE:22;
then B c= the Sorts of ((GenOSAlg A) "\/"_os U1) by A1, A5, PBOOLE:15;
then A7: B is MSSubset of ((GenOSAlg A) "\/"_os U1) by PBOOLE:def 23;
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 17;
B is OSSubset of GenOSAlg B by Def13;
then A10: B c= the Sorts of (GenOSAlg B) by PBOOLE:def 23;
A c= B by A1, PBOOLE:16;
then A c= the Sorts of (GenOSAlg B) by A10, PBOOLE:15;
then A c= the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) by A6, PBOOLE:19;
then A is MSSubset of ((GenOSAlg A) /\ (GenOSAlg B)) by A9, PBOOLE:def 23;
then A is OSSubset of (GenOSAlg A) /\ (GenOSAlg B) by A8, Def2;
then GenOSAlg A is OSSubAlgebra of (GenOSAlg A) /\ (GenOSAlg B) by Def13;
then a is MSSubset of ((GenOSAlg A) /\ (GenOSAlg B)) by MSUALG_2:def 10;
then A11: a c= the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) by A9, PBOOLE:def 23;
the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) c= a by PBOOLE:17;
then a = the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) by A11, PBOOLE:def 13;
then A12: a c= the Sorts of (GenOSAlg B) by PBOOLE:17;
u1 c= B by A1, PBOOLE:16;
then u1 c= the Sorts of (GenOSAlg B) by A10, PBOOLE:15;
then b c= the Sorts of (GenOSAlg B) by A12, PBOOLE:18;
then b is MSSubset of (GenOSAlg B) by PBOOLE:def 23;
then b is OSSubset of GenOSAlg B by A3, Def2;
then A13: GenOSAlg b is strict OSSubAlgebra of GenOSAlg B by Def13;
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 Def13;
hence (GenOSAlg A) "\/"_os U1 = GenOSAlg B by A4, A13, MSUALG_2:8; :: thesis: verum