let S be non empty non void ManySortedSign ; for U0 being non-empty MSAlgebra of S holds MSAlg_meet U0 is associative
let U0 be non-empty MSAlgebra of 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 Def20;
reconsider u23 =
U2 /\ U3,
u12 =
U1 /\ U2 as
Element of
MSSub U0 by Def20;
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 Def17;
A2:
(MSAlg_meet U0) . ((MSAlg_meet U0) . x,y),
z =
(MSAlg_meet U0) . u12,
z
by Def22
.=
(U1 /\ U2) /\ U3
by Def22
;
the
Sorts of
(U2 /\ U3) = the
Sorts of
U2 /\ the
Sorts of
U3
by Def17;
then A3:
the
Sorts of
(U1 /\ (U2 /\ U3)) = the
Sorts of
U1 /\ (the Sorts of U2 /\ the Sorts of U3)
by Def17;
then reconsider C = the
Sorts of
U1 /\ (the Sorts of U2 /\ the Sorts of U3) as
MSSubset of
U0 by Def10;
A4:
(MSAlg_meet U0) . x,
((MSAlg_meet U0) . y,z) =
(MSAlg_meet U0) . x,
u23
by Def22
.=
U1 /\ (U2 /\ U3)
by Def22
;
C = (the Sorts of U1 /\ the Sorts of U2) /\ the
Sorts of
U3
by PBOOLE:35;
hence
(MSAlg_meet U0) . x,
((MSAlg_meet U0) . y,z) = (MSAlg_meet U0) . ((MSAlg_meet U0) . x,y),
z
by A4, A2, A3, A1, Def17;
verum
end;
hence
MSAlg_meet U0 is associative
by BINOP_1:def 3; verum