theorem :: LATTICE6:10
for L being complete Lattice holds
( (Top L) *' = Top L & (Top L) % is meet-irreducible )