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)

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

hence
UniAlg_meet U0 is associative
by BINOP_1:def 3; :: thesis: verum
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 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; :: thesis: verum

end;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; :: thesis: verum