for S being lower-bounded sup-Semilattice
for x being Element of (InclPoset (Ids S)) holds
( x is compact iff x is principal Ideal of S )