theorem Th18: :: WAYBEL35:18

for L being RelStr
for R being auxiliary(i) Relation of L
for C being set
for x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L holds
x = sup (SetBelow (R,C,x))