let S1 be OrderSortedSign; for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is commutative
let U0 be non-empty OSAlgebra of S1; 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;
(OSAlg_join U0) . x,y = (OSAlg_join U0) . y,x
reconsider U1 =
x,
U2 =
y as
strict OSSubAlgebra of
U0 by Def15;
set B = the
Sorts of
U1 \/ the
Sorts of
U2;
the
Sorts of
U2 is
MSSubset of
U0
by MSUALG_2:def 10;
then A1:
the
Sorts of
U2 c= the
Sorts of
U0
by PBOOLE:def 23;
the
Sorts of
U1 is
MSSubset of
U0
by MSUALG_2:def 10;
then
the
Sorts of
U1 c= the
Sorts of
U0
by PBOOLE:def 23;
then
the
Sorts of
U1 \/ the
Sorts of
U2 c= the
Sorts of
U0
by A1, PBOOLE:18;
then A2:
the
Sorts of
U1 \/ the
Sorts of
U2 is
MSSubset of
U0
by PBOOLE:def 23;
( the
Sorts of
U1 is
OrderSortedSet of
S1 & the
Sorts of
U2 is
OrderSortedSet of
S1 )
by OSALG_1:17;
then
the
Sorts of
U1 \/ the
Sorts of
U2 is
OrderSortedSet of
S1
by Th2;
then reconsider B = the
Sorts of
U1 \/ the
Sorts of
U2 as
OSSubset of
U0 by A2, Def2;
A3:
U1 "\/"_os U2 = GenOSAlg B
by Def14;
(
(OSAlg_join U0) . x,
y = U1 "\/"_os U2 &
(OSAlg_join U0) . y,
x = U2 "\/"_os U1 )
by Def16;
hence
(OSAlg_join U0) . x,
y = (OSAlg_join U0) . y,
x
by A3, Def14;
verum
end;
hence
OSAlg_join U0 is commutative
by BINOP_1:def 2; verum