theorem :: WAYBEL23:32

for L being sup-Semilattice
for S being non empty lower Subset of L holds
( S is Ideal of L iff S is join-closed ) by WAYBEL_0:64;