theorem Th22: :: WAYBEL_6:22

for L being Semilattice
for l being Element of L holds
( l is prime iff for A being non empty finite Subset of L st l >= inf A holds
ex a being Element of L st
( a in A & l >= a ) )