let S1 be OrderSortedSign; :: thesis: for U0 being non-empty OSAlgebra of S1
for U1, U2 being strict OSSubAlgebra of U0 holds U1 /\ (U1 "\/"_os U2) = U1
let U0 be non-empty OSAlgebra of S1; :: thesis: for U1, U2 being strict OSSubAlgebra of U0 holds U1 /\ (U1 "\/"_os U2) = U1
let U1, U2 be strict OSSubAlgebra of U0; :: thesis: U1 /\ (U1 "\/"_os U2) = U1
reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def 10;
A1: ( u1 is OrderSortedSet of & u2 is OrderSortedSet of ) by OSALG_1:17;
( u1 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def 23;
then u1 \/ u2 c= the Sorts of U0 by PBOOLE:18;
then reconsider A = u1 \/ u2 as MSSubset of U0 by PBOOLE:def 23;
A is OrderSortedSet of by A1, Th2;
then reconsider A = A as OSSubset of U0 by Def2;
U1 "\/"_os U2 = GenOSAlg A by Def14;
then A is OSSubset of U1 "\/"_os U2 by Def13;
then A2: A c= the Sorts of (U1 "\/"_os U2) by PBOOLE:def 23;
the Sorts of U1 c= A by PBOOLE:16;
then A3: the Sorts of U1 c= the Sorts of (U1 "\/"_os U2) by A2, PBOOLE:15;
A4: the Sorts of (U1 /\ (U1 "\/"_os U2)) = the Sorts of U1 /\ the Sorts of (U1 "\/"_os U2) by MSUALG_2:def 17;
then A5: the Sorts of U1 c= the Sorts of (U1 /\ (U1 "\/"_os U2)) by A3, PBOOLE:19;
the Sorts of (U1 /\ (U1 "\/"_os U2)) c= the Sorts of U1 by A4, PBOOLE:17;
then A6: the Sorts of (U1 /\ (U1 "\/"_os U2)) = the Sorts of U1 by A5, PBOOLE:def 13;
reconsider u112 = the Sorts of (U1 /\ (U1 "\/"_os U2)) as MSSubset of U0 by MSUALG_2:def 10;
( u112 is opers_closed & the Charact of (U1 /\ (U1 "\/"_os U2)) = Opers U0,u112 ) by MSUALG_2:def 17;
hence U1 /\ (U1 "\/"_os U2) = U1 by A6, MSUALG_2:def 10; :: thesis: verum