theorem :: POSET_2:5

for P, Q being non empty chain-complete Poset
for L being non empty Chain of [:P,Q:] holds sup L = [(sup (proj1 L)),(sup (proj2 L))] by YELLOW_3:46, LemProdPoset06;