theorem :: WAYBEL_2:29

for L being with_suprema Poset st ( for X being directed Subset of L
for x being Element of L holds x "/\" (sup X) = sup ({x} "/\" X) ) holds
for X being Subset of L
for x being Element of L st ex_sup_of X,L holds
x "/\" (sup X) = sup ({x} "/\" (finsups X))