for L being non empty reflexive antisymmetric with_infima satisfying_MC RelStr
for x being Element of L
for D being non empty directed Subset of L st x <= sup D holds
x = sup ({x} "/\" D)