:: deftheorem Def15 defines downarrow WAYBEL_0:def 15 :
for L being RelStr
for X, b₃ being Subset of L holds
( b₃ = downarrow X iff for x being Element of L holds
( x in b₃ iff ex y being Element of L st
( y >= x & y in X ) ) );