for H being distributive complete LATTICE
for a being Element of H
for X being finite Subset of H holds a "/\" preserves_sup_of X