let S1 be OrderSortedSign; 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; for U1, U2 being strict OSSubAlgebra of U0 holds U1 /\ (U1 "\/"_os U2) = U1
let U1, U2 be strict OSSubAlgebra of U0; U1 /\ (U1 "\/"_os U2) = U1
reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def 9;
reconsider u112 = the Sorts of (U1 /\ (U1 "\/"_os U2)) as MSSubset of U0 by MSUALG_2:def 9;
A1:
the Charact of (U1 /\ (U1 "\/"_os U2)) = Opers (U0,u112)
by MSUALG_2:def 16;
( u1 c= the Sorts of U0 & u2 c= the Sorts of U0 )
by PBOOLE:def 18;
then
u1 (\/) u2 c= the Sorts of U0
by PBOOLE:16;
then reconsider A = u1 (\/) u2 as MSSubset of U0 by PBOOLE:def 18;
( u1 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1 )
by OSALG_1:17;
then
A is OrderSortedSet of S1
by Th2;
then reconsider A = A as OSSubset of U0 by Def2;
A2:
the Sorts of (U1 /\ (U1 "\/"_os U2)) = the Sorts of U1 (/\) the Sorts of (U1 "\/"_os U2)
by MSUALG_2:def 16;
U1 "\/"_os U2 = GenOSAlg A
by Def13;
then
A is OSSubset of U1 "\/"_os U2
by Def12;
then A3:
A c= the Sorts of (U1 "\/"_os U2)
by PBOOLE:def 18;
the Sorts of U1 c= A
by PBOOLE:14;
then
the Sorts of U1 c= the Sorts of (U1 "\/"_os U2)
by A3, PBOOLE:13;
then A4:
the Sorts of U1 c= the Sorts of (U1 /\ (U1 "\/"_os U2))
by A2, PBOOLE:17;
the Sorts of (U1 /\ (U1 "\/"_os U2)) c= the Sorts of U1
by A2, PBOOLE:15;
then
the Sorts of (U1 /\ (U1 "\/"_os U2)) = the Sorts of U1
by A4, PBOOLE:146;
hence
U1 /\ (U1 "\/"_os U2) = U1
by A1, MSUALG_2:def 9; verum