for H being distributive complete LATTICE
for a being Element of H
for X being finite Subset of H holds sup ({a} "/\" X) = a "/\" (sup X)