theorem ThE: :: LATSTONE:12

for L being Boolean Lattice
for x being Element of L holds x ` = x *