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 d being Element of L st d in SupBelow (R,C) holds
d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L)