theorem :: WAYBEL13:13

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