for R being complete LATTICE
for Z being net of R
for D being Subset of R st D = { ("/\" ( { (Z . k) where k is Element of Z : k >= j } ,R)) where j is Element of Z : verum } holds
( not D is empty & D is directed )