:: deftheorem Def16 defines uparrow WAYBEL_0:def 16 :
for L being RelStr
for X, b₃ being Subset of L holds
( b₃ = uparrow 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 ) ) );