let S1 be OrderSortedSign; :: thesis: for U0 being non-empty OSAlgebra of S1
for U1, U2 being strict OSSubAlgebra of U0 holds (U1 /\ U2) "\/"_os U2 = U2
let U0 be non-empty OSAlgebra of S1; :: thesis: for U1, U2 being strict OSSubAlgebra of U0 holds (U1 /\ U2) "\/"_os U2 = U2
let U1, U2 be strict OSSubAlgebra of U0; :: thesis: (U1 /\ U2) "\/"_os U2 = U2
reconsider u12 = the Sorts of (U1 /\ U2), u2 = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def 10;
A1: ( u12 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1 ) by OSALG_1:17;
then reconsider u12 = u12, u2 = u2 as OSSubset of U0 by Def2;
( u12 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def 23;
then u12 \/ u2 c= the Sorts of U0 by PBOOLE:18;
then reconsider A = u12 \/ u2 as MSSubset of U0 by PBOOLE:def 23;
A is OrderSortedSet of S1 by A1, Th2;
then reconsider A = u12 \/ u2 as OSSubset of U0 by Def2;
u12 = the Sorts of U1 /\ the Sorts of U2 by MSUALG_2:def 17;
then u12 c= u2 by PBOOLE:17;
then A2: A = u2 by PBOOLE:24;
(U1 /\ U2) "\/"_os U2 = GenOSAlg A by Def14;
hence (U1 /\ U2) "\/"_os U2 = U2 by A2, Th40; :: thesis: verum