let U0 be with_const_op Universal_Algebra; :: thesis: 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;
:: thesis: (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 Def15;
reconsider u23 =
U2 /\ U3,
u12 =
U1 /\ U2 as
Element of
Sub U0 by Def15;
A1:
(UniAlg_meet U0) . x,
((UniAlg_meet U0) . y,z) =
(UniAlg_meet U0) . x,
u23
by Def17
.=
U1 /\ (U2 /\ U3)
by Def17
;
A2:
(UniAlg_meet U0) . ((UniAlg_meet U0) . x,y),
z =
(UniAlg_meet U0) . u12,
z
by Def17
.=
(U1 /\ U2) /\ U3
by Def17
;
A3:
( the
carrier of
U1 meets the
carrier of
U2 & the
carrier of
U2 meets the
carrier of
U3 )
by Th20;
then A4:
the
carrier of
(U1 /\ U2) = the
carrier of
U1 /\ the
carrier of
U2
by Def10;
then A5:
the
carrier of
U1 /\ the
carrier of
U2 meets the
carrier of
U3
by Th20;
A6:
the
carrier of
(U2 /\ U3) = the
carrier of
U2 /\ the
carrier of
U3
by A3, Def10;
then
the
carrier of
U1 meets the
carrier of
U2 /\ the
carrier of
U3
by Th20;
then A7:
( the
carrier of
(U1 /\ (U2 /\ U3)) = the
carrier of
U1 /\ (the carrier of U2 /\ the carrier of U3) & ( 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 A6, Def10;
then reconsider C = the
carrier of
U1 /\ (the carrier of U2 /\ the carrier of U3) as non
empty Subset of
U0 by Def8;
C = (the carrier of U1 /\ the carrier of U2) /\ the
carrier of
U3
by XBOOLE_1:16;
hence
(UniAlg_meet U0) . x,
((UniAlg_meet U0) . y,z) = (UniAlg_meet U0) . ((UniAlg_meet U0) . x,y),
z
by A1, A2, A4, A5, A7, Def10;
:: thesis: verum
end;
hence
UniAlg_meet U0 is associative
by BINOP_1:def 3; :: thesis: verum