theorem :: LATTICE6:25

for L being complete Lattice
for D being Subset of L holds
( D is infimum-dense iff D % is order-generating )