let U0 be with_const_op Universal_Algebra; UniAlg_meet U0 is associative
set o = UniAlg_meet U0;
for x, y, z being Element of Sub U0 holds (UniAlg_meet U0) . (x,((UniAlg_meet U0) . (y,z))) = (UniAlg_meet U0) . (((UniAlg_meet U0) . (x,y)),z)
proof
let x,
y,
z be
Element of
Sub U0;
(UniAlg_meet U0) . (x,((UniAlg_meet U0) . (y,z))) = (UniAlg_meet U0) . (((UniAlg_meet U0) . (x,y)),z)
reconsider U1 =
x,
U2 =
y,
U3 =
z as
strict SubAlgebra of
U0 by Def14;
reconsider u23 =
U2 /\ U3,
u12 =
U1 /\ U2 as
Element of
Sub U0 by Def14;
A1:
(UniAlg_meet U0) . (
x,
((UniAlg_meet U0) . (y,z))) =
(UniAlg_meet U0) . (
x,
u23)
by Def16
.=
U1 /\ (U2 /\ U3)
by Def16
;
A2:
(UniAlg_meet U0) . (
((UniAlg_meet U0) . (x,y)),
z) =
(UniAlg_meet U0) . (
u12,
z)
by Def16
.=
(U1 /\ U2) /\ U3
by Def16
;
the
carrier of
U2 meets the
carrier of
U3
by Th17;
then A3:
the
carrier of
(U2 /\ U3) = the
carrier of
U2 /\ the
carrier of
U3
by Def9;
then A4:
the
carrier of
U1 meets the
carrier of
U2 /\ the
carrier of
U3
by Th17;
then A5:
for
B being non
empty Subset of
U0 st
B = the
carrier of
(U1 /\ (U2 /\ U3)) holds
( the
charact of
(U1 /\ (U2 /\ U3)) = Opers (
U0,
B) &
B is
opers_closed )
by A3, Def9;
A6:
the
carrier of
(U1 /\ (U2 /\ U3)) = the
carrier of
U1 /\ ( the carrier of U2 /\ the carrier of U3)
by A3, A4, Def9;
then reconsider C = the
carrier of
U1 /\ ( the carrier of U2 /\ the carrier of U3) as non
empty Subset of
U0 by Def7;
A7:
C = ( the carrier of U1 /\ the carrier of U2) /\ the
carrier of
U3
by XBOOLE_1:16;
the
carrier of
U1 meets the
carrier of
U2
by Th17;
then A8:
the
carrier of
(U1 /\ U2) = the
carrier of
U1 /\ the
carrier of
U2
by Def9;
then
the
carrier of
U1 /\ the
carrier of
U2 meets the
carrier of
U3
by Th17;
hence
(UniAlg_meet U0) . (
x,
((UniAlg_meet U0) . (y,z)))
= (UniAlg_meet U0) . (
((UniAlg_meet U0) . (x,y)),
z)
by A1, A2, A8, A6, A5, A7, Def9;
verum
end;
hence
UniAlg_meet U0 is associative
by BINOP_1:def 3; verum