let L be GAD_Lattice; :: thesis: ( L is join-commutative iff ThetaOrder L is antisymmetric )
set R = ThetaOrder L;
thus ( L is join-commutative implies ThetaOrder L is antisymmetric ) :: thesis: ( ThetaOrder L is antisymmetric implies L is join-commutative )

proof

assume L is join-commutative ; :: thesis: 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 ; :: thesis: ( [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 ) ; :: thesis: 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; :: thesis: verum

end;

hence ThetaOrder L is antisymmetric by PREFER_1:31; :: thesis: verum

end;

assume z1: ThetaOrder L is antisymmetric ; :: thesis: L is join-commutative
for x, y being Element of L holds x "/\" y = y "/\" x

proof

let x, y be Element of L; :: thesis: x "/\" y = y "/\" x
B1: (x "/\" y) "/\" (y "/\" x) = (y "/\" x) "/\" (y "/\" x) by Lem310
.= y "/\" x by IMeet ;
B2: (y "/\" x) "/\" (x "/\" y) = (x "/\" y) "/\" (x "/\" y) by Lem310
.= x "/\" y by IMeet ;
B3: [(x "/\" y),(y "/\" x)] in ThetaOrder L by B1;
[(y "/\" x),(x "/\" y)] in ThetaOrder L by B2;
hence x "/\" y = y "/\" x by z1, B3, PREFER_1:31; :: thesis: verum

end;

then L is meet-commutative ;
hence L is join-commutative by Th31145; :: thesis: verum