let U0 be with_const_op Universal_Algebra; 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)
proof
let x,
y be
Element of
Sub U0;
(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;
verum
end;
hence
UniAlg_meet U0 is commutative
by BINOP_1:def 2; verum