theorem :: LATTICES:22

for L being B_Lattice
for a being Element of L holds (a `) ` = a ;