let L be GAD_Lattice; :: thesis: ( L is join-commutative iff ( L is Lattice-like & L is distributive ) )
thus ( L is join-commutative implies ( L is Lattice-like & L is distributive ) ) :: thesis: ( L is Lattice-like & L is distributive implies L is join-commutative )

proof

assume T0: L is join-commutative ; :: thesis: ( L is Lattice-like & L is distributive )
then L is join-associative by Th14;
hence ( L is Lattice-like & L is distributive ) by T0, Th31145; :: thesis: verum

end;

thus ( L is Lattice-like & L is distributive implies L is join-commutative ) ; :: thesis: verum