for L being Lattice holds the L_join of L is_distributive_wrt the L_join of L