theorem Th12: :: WAYBEL13:12

for S being lower-bounded sup-Semilattice
for x being Element of (InclPoset (Ids S)) holds
( x is compact iff ex a being Element of S st x = downarrow a )