let S1 be OrderSortedSign; for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is associative
let U0 be non-empty OSAlgebra of S1; OSAlg_meet U0 is associative
set o = OSAlg_meet U0;
set m = MSAlg_meet U0;
A1:
MSAlg_meet U0 is associative
by MSUALG_2:32;
for x, y, z being Element of OSSub U0 holds (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z)
proof
let x,
y,
z be
Element of
OSSub U0;
(OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z)
A2:
(OSAlg_meet U0) . (
x,
y)
= (MSAlg_meet U0) . (
x,
y)
by Th43;
(OSAlg_meet U0) . (
y,
z)
= (MSAlg_meet U0) . (
y,
z)
by Th43;
then (OSAlg_meet U0) . (
x,
((OSAlg_meet U0) . (y,z))) =
(MSAlg_meet U0) . (
x,
((MSAlg_meet U0) . (y,z)))
by Th43
.=
(MSAlg_meet U0) . (
((MSAlg_meet U0) . (x,y)),
z)
by A1, BINOP_1:def 3
.=
(OSAlg_meet U0) . (
((OSAlg_meet U0) . (x,y)),
z)
by A2, Th43
;
hence
(OSAlg_meet U0) . (
x,
((OSAlg_meet U0) . (y,z)))
= (OSAlg_meet U0) . (
((OSAlg_meet U0) . (x,y)),
z)
;
verum
end;
hence
OSAlg_meet U0 is associative
by BINOP_1:def 3; verum