for L being complete LATTICE
for A being Subset of L st A is lower holds
( A ` in xi L iff A is closed_under_directed_sups )