theorem Th24: :: WAYBEL13:24

for L being lower-bounded algebraic LATTICE ex g being Function of L,(BoolePoset the carrier of (CompactSublatt L)) st
( g is infs-preserving & g is directed-sups-preserving & g is one-to-one & ( for x being Element of L holds g . x = compactbelow x ) )