let L be GAD_Lattice; ( L is join-commutative iff ThetaOrder L is antisymmetric )
set R = ThetaOrder L;
thus
( L is join-commutative implies ThetaOrder L is antisymmetric )
( ThetaOrder L is antisymmetric implies L is join-commutative )proof
assume
L is
join-commutative
;
ThetaOrder L is antisymmetric
then A0:
L is
meet-commutative
by Th31145;
for
x,
y being
object st
[x,y] in ThetaOrder L &
[y,x] in ThetaOrder L holds
x = y
proof
let x,
y be
object ;
( [x,y] in ThetaOrder L & [y,x] in ThetaOrder L implies x = y )
assume A1:
(
[x,y] in ThetaOrder L &
[y,x] in ThetaOrder L )
;
x = y
then consider xx,
yy being
Element of
L such that A3:
(
[x,y] = [xx,yy] &
xx "/\" yy = yy )
;
A4:
(
x = xx &
y = yy )
by A3, XTUPLE_0:1;
(
xx "/\" yy = yy &
yy "/\" xx = xx )
by ThetaOrdLat, A1, A4;
hence
x = y
by A4, A0;
verum
end;
hence
ThetaOrder L is
antisymmetric
by PREFER_1:31;
verum
end;
assume z1:
ThetaOrder L is antisymmetric
; L is join-commutative
for x, y being Element of L holds x "/\" y = y "/\" x
then
L is meet-commutative
;
hence
L is join-commutative
by Th31145; verum