theorem Th16: :: WAYBEL13:16

for L being lower-bounded algebraic sup-Semilattice
for f being Function of L,(InclPoset (Ids (CompactSublatt L))) st ( for x being Element of L holds f . x = compactbelow x ) holds
f is isomorphic