for L being lower-bounded algebraic sup-Semilattice
for x being Element of L holds
( compactbelow x is principal Ideal of (CompactSublatt L) iff x is compact )