theorem :: WAYBEL_4:14
for a being set
for L being sup-Semilattice
for AR being Relation of L
for y being Element of L holds
( a in AR -above y iff [y,a] in AR )