theorem :: YELLOW_4:28

for L being non empty complete Poset
for A, B being non empty Subset of L holds sup (A "\/" B) = (sup A) "\/" (sup B)