theorem Th11: :: POSET_1:11

for P, Q being non empty strict chain-complete Poset
for F being non empty Chain of (ConPoset (P,Q)) holds
( ex_sup_of F, ConPoset (P,Q) & sup_func F = "\/" (F,(ConPoset (P,Q))) )