for L being complete Lattice
for a being Element of L holds
( a [= a *' & *' a [= a )