theorem Th19: :: WAYBEL35:19

for L being non empty complete Poset
for R being extra-order Relation of L
for C being satisfying_SIC strict_chain of R
for p, q being Element of L st p in C & q in C & p < q holds
ex y being Element of L st
( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) )