theorem :: WAYBEL35:21

for L being non empty reflexive antisymmetric RelStr
for R being auxiliary(i) Relation of L
for C being strict_chain of R st ( for c being Element of L st c in C holds
( ex_sup_of SetBelow (R,C,c),L & c = sup (SetBelow (R,C,c)) ) ) holds
R satisfies_SIC_on C