for L being 1_Lattice holds Top L = the_unity_wrt the L_meet of L by Th19;