let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is associative
let U0 be non-empty MSAlgebra over S; :: thesis:
set o = MSAlg_meet U0;
for x, y, z being Element of MSSub U0 holds () . (x,(() . (y,z))) = () . ((() . (x,y)),z)
proof
let x, y, z be Element of MSSub U0; :: thesis: () . (x,(() . (y,z))) = () . ((() . (x,y)),z)
reconsider U1 = x, U2 = y, U3 = z as strict MSSubAlgebra of U0 by Def19;
reconsider u23 = U2 /\ U3, u12 = U1 /\ U2 as Element of MSSub U0 by Def19;
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 Def16;
A2: () . ((() . (x,y)),z) = () . (u12,z) by Def21
.= (U1 /\ U2) /\ U3 by Def21 ;
the Sorts of (U2 /\ U3) = the Sorts of U2 (/\) the Sorts of U3 by Def16;
then A3: the Sorts of (U1 /\ (U2 /\ U3)) = the Sorts of U1 (/\) ( the Sorts of U2 (/\) the Sorts of U3) by Def16;
then reconsider C = the Sorts of U1 (/\) ( the Sorts of U2 (/\) the Sorts of U3) as MSSubset of U0 by Def9;
A4: () . (x,(() . (y,z))) = () . (x,u23) by Def21
.= U1 /\ (U2 /\ U3) by Def21 ;
C = ( the Sorts of U1 (/\) the Sorts of U2) (/\) the Sorts of U3 by PBOOLE:29;
hence (MSAlg_meet U0) . (x,(() . (y,z))) = () . ((() . (x,y)),z) by A4, A2, A3, A1, Def16; :: thesis: verum
end;
hence MSAlg_meet U0 is associative by BINOP_1:def 3; :: thesis: verum