theorem :: LATTAD_1:52
for L being GAD_Lattice holds
( L is join-commutative iff LatRelStr L is directed )