theorem :: WAYBEL23:31

for L being Semilattice
for S being non empty upper Subset of L holds
( S is Filter of L iff S is meet-closed ) by WAYBEL_0:63;