theorem :: YELLOW_4:53

for L being Semilattice
for X being Subset of L
for x being Element of L st ex_sup_of {x} "/\" X,L & ex_sup_of X,L holds
sup ({x} "/\" X) <= x "/\" (sup X)