theorem :: LATTICES:18

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