theorem :: WAYBEL31:14

for L1 being non empty reflexive RelStr
for a being Element of L1 holds Way_Up (a,({} L1)) = wayabove a ;