let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S holds MSAlg_meet U0 is commutative

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

set o = MSAlg_meet U0;

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

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

set o = MSAlg_meet U0;

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

proof

hence
MSAlg_meet U0 is commutative
by BINOP_1:def 2; :: thesis: verum
let x, y be Element of MSSub U0; :: thesis: (MSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (y,x)

reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;

A1: ( the Sorts of (U2 /\ U1) = the Sorts of U2 (/\) the Sorts of U1 & ( for B2 being MSSubset of U0 st B2 = the Sorts of (U2 /\ U1) holds

( B2 is opers_closed & the Charact of (U2 /\ U1) = Opers (U0,B2) ) ) ) by Def16;

( (MSAlg_meet U0) . (x,y) = U1 /\ U2 & (MSAlg_meet U0) . (y,x) = U2 /\ U1 ) by Def21;

hence (MSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (y,x) by A1, Def16; :: thesis: verum

end;reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;

A1: ( the Sorts of (U2 /\ U1) = the Sorts of U2 (/\) the Sorts of U1 & ( for B2 being MSSubset of U0 st B2 = the Sorts of (U2 /\ U1) holds

( B2 is opers_closed & the Charact of (U2 /\ U1) = Opers (U0,B2) ) ) ) by Def16;

( (MSAlg_meet U0) . (x,y) = U1 /\ U2 & (MSAlg_meet U0) . (y,x) = U2 /\ U1 ) by Def21;

hence (MSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (y,x) by A1, Def16; :: thesis: verum