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