theorem :: LATTICE6:27

for L being complete Lattice
for D being Subset of L st D is infimum-dense holds
MIRRS L c= D