for L being with_suprema Poset
for X being Subset of L
for x being Element of L st ex_inf_of {x} "\/" X,L & ex_inf_of X,L holds
x "\/" (inf X) <= inf ({x} "\/" X)