:: deftheorem defines -below WAYBEL_4:def 10 :
for L being non empty RelStr
for x being Element of L
for AR being Relation of the carrier of L holds AR -below x = { y where y is Element of L : [y,x] in AR } ;