let U0 be with_const_op Universal_Algebra; :: thesis: UniAlg_meet U0 is commutative

set o = UniAlg_meet U0;

for x, y being Element of Sub U0 holds (UniAlg_meet U0) . (x,y) = (UniAlg_meet U0) . (y,x)

set o = UniAlg_meet U0;

for x, y being Element of Sub U0 holds (UniAlg_meet U0) . (x,y) = (UniAlg_meet U0) . (y,x)

proof

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

reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14;

A1: ( (UniAlg_meet U0) . (x,y) = U1 /\ U2 & (UniAlg_meet U0) . (y,x) = U2 /\ U1 ) by Def16;

A2: the carrier of U1 meets the carrier of U2 by Th17;

then ( the carrier of (U2 /\ U1) = the carrier of U2 /\ the carrier of U1 & ( for B2 being non empty Subset of U0 st B2 = the carrier of (U2 /\ U1) holds

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

hence (UniAlg_meet U0) . (x,y) = (UniAlg_meet U0) . (y,x) by A1, A2, Def9; :: thesis: verum

end;reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def14;

A1: ( (UniAlg_meet U0) . (x,y) = U1 /\ U2 & (UniAlg_meet U0) . (y,x) = U2 /\ U1 ) by Def16;

A2: the carrier of U1 meets the carrier of U2 by Th17;

then ( the carrier of (U2 /\ U1) = the carrier of U2 /\ the carrier of U1 & ( for B2 being non empty Subset of U0 st B2 = the carrier of (U2 /\ U1) holds

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

hence (UniAlg_meet U0) . (x,y) = (UniAlg_meet U0) . (y,x) by A1, A2, Def9; :: thesis: verum