:: deftheorem Def10 defines SupBelow WAYBEL35:def 10 :
for L being non empty RelStr
for R being Relation of the carrier of L
for C, b₄ being set holds
( b₄ = SupBelow (R,C) iff for y being set holds
( y in b₄ iff y = sup (SetBelow (R,C,y)) ) );