theorem :: LATTICE6:11
for L being complete Lattice holds
( *' (Bottom L) = Bottom L & (Bottom L) % is join-irreducible )