let U0 be with_const_op Universal_Algebra; :: thesis:
set o = UniAlg_meet U0;
for x, y, z being Element of Sub U0 holds () . (x,(() . (y,z))) = () . ((() . (x,y)),z)
proof
let x, y, z be Element of Sub U0; :: thesis: () . (x,(() . (y,z))) = () . ((() . (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: () . (x,(() . (y,z))) = () . (x,u23) by Def16
.= U1 /\ (U2 /\ U3) by Def16 ;
A2: () . ((() . (x,y)),z) = () . (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 ;
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,(() . (y,z))) = () . ((() . (x,y)),z) by A1, A2, A8, A6, A5, A7, Def9; :: thesis: verum
end;
hence UniAlg_meet U0 is associative by BINOP_1:def 3; :: thesis: verum