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