let S be non empty non void ManySortedSign ; for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is associative
let U0 be non-empty MSAlgebra over S; MSAlg_meet U0 is associative
set o = MSAlg_meet U0;
for x, y, z being Element of MSSub U0 holds (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z)
proof
let x,
y,
z be
Element of
MSSub U0;
(MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z)
reconsider U1 =
x,
U2 =
y,
U3 =
z as
strict MSSubAlgebra of
U0 by Def19;
reconsider u23 =
U2 /\ U3,
u12 =
U1 /\ U2 as
Element of
MSSub U0 by Def19;
A1:
( the
Sorts of
(U1 /\ U2) = the
Sorts of
U1 (/\) the
Sorts of
U2 & ( for
B being
MSSubset of
U0 st
B = the
Sorts of
(U1 /\ (U2 /\ U3)) holds
(
B is
opers_closed & the
Charact of
(U1 /\ (U2 /\ U3)) = Opers (
U0,
B) ) ) )
by Def16;
A2:
(MSAlg_meet U0) . (
((MSAlg_meet U0) . (x,y)),
z) =
(MSAlg_meet U0) . (
u12,
z)
by Def21
.=
(U1 /\ U2) /\ U3
by Def21
;
the
Sorts of
(U2 /\ U3) = the
Sorts of
U2 (/\) the
Sorts of
U3
by Def16;
then A3:
the
Sorts of
(U1 /\ (U2 /\ U3)) = the
Sorts of
U1 (/\) ( the Sorts of U2 (/\) the Sorts of U3)
by Def16;
then reconsider C = the
Sorts of
U1 (/\) ( the Sorts of U2 (/\) the Sorts of U3) as
MSSubset of
U0 by Def9;
A4:
(MSAlg_meet U0) . (
x,
((MSAlg_meet U0) . (y,z))) =
(MSAlg_meet U0) . (
x,
u23)
by Def21
.=
U1 /\ (U2 /\ U3)
by Def21
;
C = ( the Sorts of U1 (/\) the Sorts of U2) (/\) the
Sorts of
U3
by PBOOLE:29;
hence
(MSAlg_meet U0) . (
x,
((MSAlg_meet U0) . (y,z)))
= (MSAlg_meet U0) . (
((MSAlg_meet U0) . (x,y)),
z)
by A4, A2, A3, A1, Def16;
verum
end;
hence
MSAlg_meet U0 is associative
by BINOP_1:def 3; verum