theorem :: WAYBEL_2:52

for L being up-complete LATTICE holds
( L is meet-continuous iff for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D) )