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 Def15;
A1:
(
(UniAlg_meet U0) . x,
y = U1 /\ U2 &
(UniAlg_meet U0) . y,
x = U2 /\ U1 )
by Def17;
A2:
the
carrier of
U1 meets the
carrier of
U2
by Th20;
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 Def10;
hence
(UniAlg_meet U0) . x,
y = (UniAlg_meet U0) . y,
x
by A1, A2, Def10;
verum
end;
hence
UniAlg_meet U0 is commutative
by BINOP_1:def 2; verum