theorem Th13: :: WAYBEL_4:13

for L being non empty RelStr
for AR being Relation of L
for a being object
for y being Element of L holds
( a in AR -below y iff [a,y] in AR )