let S1 be OrderSortedSign; :: thesis: for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is commutative
let U0 be non-empty OSAlgebra of S1; :: thesis: OSAlg_join U0 is commutative
set o = OSAlg_join U0;
for x, y being Element of OSSub U0 holds (OSAlg_join U0) . x,y = (OSAlg_join U0) . y,x

proof

let x, y be Element of OSSub U0; :: thesis: (OSAlg_join U0) . x,y = (OSAlg_join U0) . y,x
reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def15;
A1: ( (OSAlg_join U0) . x,y = U1 "\/"_os U2 & (OSAlg_join U0) . y,x = U2 "\/"_os U1 ) by Def16;
set B = the Sorts of U1 \/ the Sorts of U2;
( the Sorts of U1 is OrderSortedSet of & the Sorts of U2 is OrderSortedSet of ) by OSALG_1:17;
then A2: the Sorts of U1 \/ the Sorts of U2 is OrderSortedSet of by Th2;
( the Sorts of U1 is MSSubset of U0 & the Sorts of U2 is MSSubset of U0 ) by MSUALG_2:def 10;
then ( the Sorts of U1 c= the Sorts of U0 & the Sorts of U2 c= the Sorts of U0 ) by PBOOLE:def 23;
then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by PBOOLE:18;
then the Sorts of U1 \/ the Sorts of U2 is MSSubset of U0 by PBOOLE:def 23;
then reconsider B = the Sorts of U1 \/ the Sorts of U2 as OSSubset of U0 by A2, Def2;
( U1 "\/"_os U2 = GenOSAlg B & U2 "\/"_os U1 = GenOSAlg B ) by Def14;
hence (OSAlg_join U0) . x,y = (OSAlg_join U0) . y,x by A1; :: thesis: verum

end;

hence OSAlg_join U0 is commutative by BINOP_1:def 2; :: thesis: verum