theorem Th23: :: WAYBEL_6:23

for L being sup-Semilattice
for x being Element of L holds
( x is co-prime iff for A being non empty finite Subset of L st x <= sup A holds
ex a being Element of L st
( a in A & x <= a ) )