for L being 1_Lattice holds Top L is_a_unity_wrt the L_meet of L