for L being Lattice st the L_meet of L is having_a_unity holds
Top L = the_unity_wrt the L_meet of L