for L being antisymmetric with_suprema RelStr
for F being Subset-Family of L st ( for X being Subset of L st X in F holds
( X is lower & X is directed ) ) holds
meet F is directed Subset of L