theorem Th31141: :: LATTAD_1:51

for L being GAD_Lattice holds
( L is join-commutative iff ( L is Lattice-like & L is distributive ) )