let S1 be OrderSortedSign; :: thesis: for U0 being non-empty OSAlgebra of S1
for U1, U2 being OSSubAlgebra of U0 holds U1 "\/"_os U2 = U2 "\/"_os U1
let U0 be non-empty OSAlgebra of S1; :: thesis: for U1, U2 being OSSubAlgebra of U0 holds U1 "\/"_os U2 = U2 "\/"_os U1
let U1, U2 be OSSubAlgebra of U0; :: thesis: U1 "\/"_os U2 = U2 "\/"_os U1
reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def 9;
( 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 A1 = 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 A1 is OrderSortedSet of S1 by Th2;
then reconsider A = A1 as OSSubset of U0 by Def2;
U1 "\/"_os U2 = GenOSAlg A by Def14;
hence U1 "\/"_os U2 = U2 "\/"_os U1 by Def14; :: thesis: verum