let S be non empty non void ManySortedSign ; for U0 being non-empty MSAlgebra of S holds MSAlg_meet U0 is commutative
let U0 be non-empty MSAlgebra of S; 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
let x,
y be
Element of
MSSub U0;
(MSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (y,x)
reconsider U1 =
x,
U2 =
y as
strict MSSubAlgebra of
U0 by Def20;
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 Def17;
(
(MSAlg_meet U0) . (
x,
y)
= U1 /\ U2 &
(MSAlg_meet U0) . (
y,
x)
= U2 /\ U1 )
by Def22;
hence
(MSAlg_meet U0) . (
x,
y)
= (MSAlg_meet U0) . (
y,
x)
by A1, Def17;
verum
end;
hence
MSAlg_meet U0 is commutative
by BINOP_1:def 2; verum