theorem :: LATTICES:17

for L being 1_Lattice
for a being Element of L holds (Top L) "/\" a = a ;