for L being 1_Lattice
for a being Element of L holds a [= Top L