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