theorem Th16: :: WAYBEL35:16

for L being RelStr
for R being auxiliary(i) Relation of L
for C being set
for y being Element of L holds SetBelow (R,C,y) is_<=_than y