:: deftheorem defines downarrow WAYBEL_0:def 17 :
for L being non empty RelStr
for x being Element of L holds downarrow x = downarrow {x};