for L being Lattice
for S being non empty initial final Subset of L holds S = [#] L