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