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