for L being 0_Lattice holds Bottom L is_a_unity_wrt the L_join of L