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: MSAlg_meet U0 is associative

set o = MSAlg_meet U0;

for x, y, z being Element of MSSub U0 holds (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z)

let U0 be non-empty MSAlgebra over S; :: thesis: MSAlg_meet U0 is associative

set o = MSAlg_meet U0;

for x, y, z being Element of MSSub U0 holds (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z)

proof

hence
MSAlg_meet U0 is associative
by BINOP_1:def 3; :: thesis: verum
let x, y, z be Element of MSSub U0; :: thesis: (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (((MSAlg_meet U0) . (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: (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z) = (MSAlg_meet U0) . (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: (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (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,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z) by A4, A2, A3, A1, Def16; :: thesis: verum

end;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: (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z) = (MSAlg_meet U0) . (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: (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (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,((MSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z) by A4, A2, A3, A1, Def16; :: thesis: verum