theorem Th9: :: LATTICE6:9

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