theorem Th31146: :: LATTAD_1:55

for L being GAD_Lattice holds
( L is join-commutative iff ThetaOrder L is antisymmetric )